Documentation Verification Report

OrderIso

📁 Source: Mathlib/Algebra/Order/GroupWithZero/Unbundled/OrderIso.lean

Statistics

Metric	Count
Definitions `divRight₀`, `mulLeft₀`, `mulRight₀`	3
Theorems `divRight₀_apply`, `divRight₀_symm_apply`, `mulLeft₀_apply`, `mulLeft₀_symm`, `mulLeft₀_symm_apply`, `mulRight₀_apply`, `mulRight₀_symm`, `mulRight₀_symm_apply`, `inf_mul₀`, `mul_inf₀`, `mul_sup₀`, `sup_mul₀`	12
Total	15

OrderIso

Definitions

Name	Category	Theorems
`divRight₀` 📖	CompOp	2 math math: `divRight₀_symm_apply`, `divRight₀_apply`
`mulLeft₀` 📖	CompOp	3 math math: `mulLeft₀_apply`, `mulLeft₀_symm_apply`, `mulLeft₀_symm`
`mulRight₀` 📖	CompOp	3 math math: `mulRight₀_symm_apply`, `mulRight₀_symm`, `mulRight₀_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`divRight₀_apply` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`DFunLike.coe` `RelIso` `Preorder.toLE` `RelIso.instFunLike` `divRight₀` `DivInvMonoid.toDiv` `GroupWithZero.toDivInvMonoid`	—	—
`divRight₀_symm_apply` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`DFunLike.coe` `RelIso` `Preorder.toLE` `RelIso.instFunLike` `RelIso.symm` `divRight₀` `MulZeroClass.toMul`	—	—
`mulLeft₀_apply` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`DFunLike.coe` `RelIso` `Preorder.toLE` `RelIso.instFunLike` `mulLeft₀` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid`	—	—
`mulLeft₀_symm` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`symm` `Preorder.toLE` `mulLeft₀` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `inv_pos`	—	`ext` `inv_pos`
`mulLeft₀_symm_apply` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`DFunLike.coe` `RelIso` `Preorder.toLE` `RelIso.instFunLike` `RelIso.symm` `mulLeft₀` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `DivInvMonoid.toInv` `DivisionMonoid.toDivInvMonoid` `GroupWithZero.toDivisionMonoid`	—	`Units.val_inv_eq_inv_val`
`mulRight₀_apply` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`DFunLike.coe` `RelIso` `Preorder.toLE` `RelIso.instFunLike` `mulRight₀` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid`	—	—
`mulRight₀_symm` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`symm` `Preorder.toLE` `mulRight₀` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid` `Right.inv_pos`	—	`ext` `Right.inv_pos`
`mulRight₀_symm_apply` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`DFunLike.coe` `RelIso` `Preorder.toLE` `RelIso.instFunLike` `RelIso.symm` `mulRight₀` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `DivInvMonoid.toInv` `DivisionMonoid.toDivInvMonoid` `GroupWithZero.toDivisionMonoid`	—	`Units.val_inv_eq_inv_val`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inf_mul₀` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`MulZeroClass.toMul` `SemilatticeInf.toMin`	—	`LE.le.eq_or_lt` `MulZeroClass.mul_zero` `inf_of_le_left` `OrderIso.map_inf`
`mul_inf₀` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`MulZeroClass.toMul` `SemilatticeInf.toMin`	—	`LE.le.eq_or_lt` `MulZeroClass.zero_mul` `inf_of_le_left` `OrderIso.map_inf`
`mul_sup₀` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`MulZeroClass.toMul` `SemilatticeSup.toMax`	—	`LE.le.eq_or_lt` `MulZeroClass.zero_mul` `sup_of_le_left` `OrderIso.map_sup`
`sup_mul₀` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass` `MonoidWithZero.toMulZeroOneClass` `GroupWithZero.toMonoidWithZero`	`MulZeroClass.toMul` `SemilatticeSup.toMax`	—	`LE.le.eq_or_lt` `MulZeroClass.mul_zero` `sup_of_le_left` `OrderIso.map_sup`

---

← Back to Index