Documentation Verification Report

Lex

📁 Source: Mathlib/Algebra/Order/GroupWithZero/Lex.lean

Statistics

Metric	Count
Definitions `fst`, `inl`, `inr`	3
Theorems `fst_apply`, `fst_comp_inl`, `inl_apply`, `inl_eq_coe_inlₗ`, `inl_mul_inr_eq_coe_toLex`, `inr_apply`, `inr_eq_coe_inrₗ`, `fst_mono`, `inl_mono`, `inl_strictMono`, `inr_mono`, `inr_strictMono`, `snd_mono`	13
Total	16

LinearOrderedCommGroupWithZero

Definitions

Name	Category	Theorems
`fst` 📖	CompOp	2 math math: `fst_comp_inl`, `fst_apply`
`inl` 📖	CompOp	4 math math: `inl_mul_inr_eq_coe_toLex`, `inl_eq_coe_inlₗ`, `fst_comp_inl`, `inl_apply`
`inr` 📖	CompOp	3 math math: `inl_mul_inr_eq_coe_toLex`, `inr_eq_coe_inrₗ`, `inr_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidWithZeroHom` `WithZero` `Lex` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `toCommGroupWithZero` `WithZero.instPreorder` `Prod.Lex.instPreorder` `Units.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `toLinearOrderedCommMonoidWithZero` `WithZero.instMulZeroOneClass` `instMulOneClassLex` `Prod.instMulOneClass` `Units.instMulOneClass` `MonoidWithZero.toMulZeroOneClass` `OrderMonoidWithZeroHom.instFunLike` `fst` `MonoidWithZeroHom` `MonoidWithZeroHom.funLike` `MonoidWithZeroHom.fst` `WithZero.map'` `MonoidHomClass.toMonoidHom` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `ofLexMulEquiv`	—	—
`fst_comp_inl` 📖	mathematical	—	`OrderMonoidWithZeroHom.comp` `WithZero` `Lex` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `toCommGroupWithZero` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `toLinearOrderedCommMonoidWithZero` `WithZero.instPreorder` `Prod.Lex.instPreorder` `Units.instPreorder` `MonoidWithZero.toMulZeroOneClass` `WithZero.instMulZeroOneClass` `instMulOneClassLex` `Prod.instMulOneClass` `Units.instMulOneClass` `fst` `inl` `OrderMonoidWithZeroHom.id`	—	`OrderMonoidWithZeroHom.ext` `GroupWithZero.eq_zero_or_unit` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `MonoidWithZeroHom.inl_apply_unit` `MonoidWithZeroHom.fst_apply_coe`
`inl_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidWithZeroHom` `WithZero` `Lex` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `toCommGroupWithZero` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `toLinearOrderedCommMonoidWithZero` `WithZero.instPreorder` `Prod.Lex.instPreorder` `Units.instPreorder` `MonoidWithZero.toMulZeroOneClass` `WithZero.instMulZeroOneClass` `instMulOneClassLex` `Prod.instMulOneClass` `Units.instMulOneClass` `OrderMonoidWithZeroHom.instFunLike` `inl` `MonoidWithZeroHom` `MonoidWithZeroHom.funLike` `WithZero.map'` `MonoidHomClass.toMonoidHom` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `toLexMulEquiv` `MonoidWithZeroHom.inl` `LinearOrder.toDecidableEq` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass`	—	—
`inl_eq_coe_inlₗ` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidWithZeroHom` `WithZero` `Lex` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `toCommGroupWithZero` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `toLinearOrderedCommMonoidWithZero` `WithZero.instPreorder` `Prod.Lex.instPreorder` `Units.instPreorder` `MonoidWithZero.toMulZeroOneClass` `WithZero.instMulZeroOneClass` `instMulOneClassLex` `Prod.instMulOneClass` `Units.instMulOneClass` `OrderMonoidWithZeroHom.instFunLike` `inl` `WithZero.coe` `OrderMonoidHom` `Units.instPartialOrderUnits` `Monoid.toMulOneClass` `Units.instMonoid` `OrderMonoidHom.instFunLike` `OrderMonoidHom.inlₗ`	—	`CanLift.prf` `instCanLiftUnitsValIsUnit` `isUnit_iff_ne_zero` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `MonoidWithZeroHom.inl_apply_unit`
`inl_mul_inr_eq_coe_toLex` 📖	mathematical	—	`WithZero` `Lex` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `toCommGroupWithZero` `MulZeroClass.toMul` `WithZero.instMulZeroClass` `instMulLex` `Prod.instMul` `Units.instMul` `DFunLike.coe` `OrderMonoidWithZeroHom` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `toLinearOrderedCommMonoidWithZero` `WithZero.instPreorder` `Prod.Lex.instPreorder` `Units.instPreorder` `MonoidWithZero.toMulZeroOneClass` `WithZero.instMulZeroOneClass` `instMulOneClassLex` `Prod.instMulOneClass` `Units.instMulOneClass` `OrderMonoidWithZeroHom.instFunLike` `inl` `inr` `WithZero.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `toLex`	—	`inl_eq_coe_inlₗ` `inr_eq_coe_inrₗ` `WithZero.coe_mul` `OrderMonoidHom.inlₗ_mul_inrₗ_eq_toLex`
`inr_apply` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidWithZeroHom` `WithZero` `Lex` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `toCommGroupWithZero` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `toLinearOrderedCommMonoidWithZero` `WithZero.instPreorder` `Prod.Lex.instPreorder` `Units.instPreorder` `MonoidWithZero.toMulZeroOneClass` `WithZero.instMulZeroOneClass` `instMulOneClassLex` `Prod.instMulOneClass` `Units.instMulOneClass` `OrderMonoidWithZeroHom.instFunLike` `inr` `MonoidWithZeroHom` `MonoidWithZeroHom.funLike` `WithZero.map'` `MonoidHomClass.toMonoidHom` `MulEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `toLexMulEquiv` `MonoidWithZeroHom.inr` `LinearOrder.toDecidableEq` `MulZeroClass.toZero` `MulZeroOneClass.toMulZeroClass`	—	—
`inr_eq_coe_inrₗ` 📖	mathematical	—	`DFunLike.coe` `OrderMonoidWithZeroHom` `WithZero` `Lex` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `toCommGroupWithZero` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `toLinearOrderedCommMonoidWithZero` `WithZero.instPreorder` `Prod.Lex.instPreorder` `Units.instPreorder` `MonoidWithZero.toMulZeroOneClass` `WithZero.instMulZeroOneClass` `instMulOneClassLex` `Prod.instMulOneClass` `Units.instMulOneClass` `OrderMonoidWithZeroHom.instFunLike` `inr` `WithZero.coe` `OrderMonoidHom` `Units.instPartialOrderUnits` `Monoid.toMulOneClass` `Units.instMonoid` `OrderMonoidHom.instFunLike` `OrderMonoidHom.inrₗ`	—	`CanLift.prf` `instCanLiftUnitsValIsUnit` `isUnit_iff_ne_zero` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `MonoidWithZeroHom.inr_apply_unit`

MonoidWithZeroHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fst_mono` 📖	mathematical	—	`Monotone` `WithZero` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `WithZero.instPreorder` `Prod.instPreorder` `Units.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `MonoidWithZeroHom` `WithZero.instMulZeroOneClass` `Prod.instMulOneClass` `Units.instMulOneClass` `MonoidWithZero.toMulZeroOneClass` `funLike` `fst`	—	`WithZero.forall` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `monoidWithZeroHomClass` `fst_apply_coe` `GroupWithZero.toNontrivial`
`inl_mono` 📖	mathematical	—	`Monotone` `WithZero` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `WithZero.instPreorder` `Prod.instPreorder` `Units.instPreorder` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `WithZero.instMulZeroOneClass` `Prod.instMulOneClass` `Units.instMulOneClass` `funLike` `inl`	—	`Monotone.comp` `WithZero.map'_mono` `MonoidHom.inl_mono` `GroupWithZero.eq_zero_or_unit` `GroupWithZero.toNontrivial` `IsOrderedMonoid.toIsOrderedCancelMonoid` `Units.isOrderedMonoid` `LinearOrderedCommMonoidWithZero.toIsOrderedMonoid`
`inl_strictMono` 📖	mathematical	—	`StrictMono` `WithZero` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `WithZero.instPreorder` `Prod.instPreorder` `Units.instPreorder` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `WithZero.instMulZeroOneClass` `Prod.instMulOneClass` `Units.instMulOneClass` `funLike` `inl`	—	`Monotone.strictMono_of_injective` `inl_mono` `inl_injective`
`inr_mono` 📖	mathematical	—	`Monotone` `WithZero` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `WithZero.instPreorder` `Prod.instPreorder` `Units.instPreorder` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `WithZero.instMulZeroOneClass` `Prod.instMulOneClass` `Units.instMulOneClass` `funLike` `inr`	—	`Monotone.comp` `WithZero.map'_mono` `MonoidHom.inr_mono` `GroupWithZero.eq_zero_or_unit` `GroupWithZero.toNontrivial` `IsOrderedMonoid.toIsOrderedCancelMonoid` `Units.isOrderedMonoid` `LinearOrderedCommMonoidWithZero.toIsOrderedMonoid`
`inr_strictMono` 📖	mathematical	—	`StrictMono` `WithZero` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `WithZero.instPreorder` `Prod.instPreorder` `Units.instPreorder` `DFunLike.coe` `MonoidWithZeroHom` `MonoidWithZero.toMulZeroOneClass` `WithZero.instMulZeroOneClass` `Prod.instMulOneClass` `Units.instMulOneClass` `funLike` `inr`	—	`Monotone.strictMono_of_injective` `inr_mono` `inr_injective`
`snd_mono` 📖	mathematical	—	`Monotone` `WithZero` `Units` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `CommGroupWithZero.toGroupWithZero` `LinearOrderedCommGroupWithZero.toCommGroupWithZero` `WithZero.instPreorder` `Prod.instPreorder` `Units.instPreorder` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `LinearOrderedCommMonoidWithZero.toLinearOrder` `LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero` `DFunLike.coe` `MonoidWithZeroHom` `WithZero.instMulZeroOneClass` `Prod.instMulOneClass` `Units.instMulOneClass` `MonoidWithZero.toMulZeroOneClass` `funLike` `snd`	—	`WithZero.forall` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `monoidWithZeroHomClass` `snd_apply_coe` `GroupWithZero.toNontrivial`

---

← Back to Index