Units

📁 Source: Mathlib/Algebra/Order/Hom/Units.lean

Statistics

Metric	Count
Definitions unitsCongr	1
Theorems val_inv_unitsCongr_apply, val_inv_unitsCongr_symm_apply, val_unitsCongr_apply, val_unitsCongr_symm_apply	4
Total	5

OrderMonoidIso

Definitions

Name	Category	Theorems
unitsCongr 📖	CompOp	4 math math: val_unitsCongr_symm_apply, val_unitsCongr_apply, val_inv_unitsCongr_symm_apply, val_inv_unitsCongr_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
val_inv_unitsCongr_apply 📖	mathematical	—	Units.val Units Units.instInv DFunLike.coe OrderMonoidIso Units.instPreorder Units.instMul EquivLike.toFunLike instEquivLike unitsCongr MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—
val_inv_unitsCongr_symm_apply 📖	mathematical	—	Units.val Units Units.instInv DFunLike.coe OrderMonoidIso Units.instPreorder Units.instMul EquivLike.toFunLike instEquivLike symm unitsCongr MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MulEquiv.instEquivLike MulEquiv.symm MulEquivClass.toMulEquiv instMulEquivClass	—	—
val_unitsCongr_apply 📖	mathematical	—	Units.val DFunLike.coe OrderMonoidIso Units Units.instPreorder Units.instMul EquivLike.toFunLike instEquivLike unitsCongr MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	—	—
val_unitsCongr_symm_apply 📖	mathematical	—	Units.val DFunLike.coe OrderMonoidIso Units Units.instPreorder Units.instMul EquivLike.toFunLike instEquivLike symm unitsCongr MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MulEquiv.instEquivLike MulEquiv.symm MulEquivClass.toMulEquiv instMulEquivClass	—	—

---

← Back to Index