WithZero

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

Statistics

Metric	Count
Definitions withZeroUnits	1
Theorems withZeroUnits_apply, withZeroUnits_symm_apply, withZeroUnitsEquiv_strictMono, withZeroUnitsEquiv_symm_strictMono, instMulPosMonoWithZeroOfMulRightMono, instMulPosStrictMonoWithZeroOfMulRightStrictMono, instPosMulMonoWithZeroOfMulLeftMono, instPosMulStrictMonoWithZeroOfMulLeftStrictMono	8
Total	9

OrderIso

Definitions

Name	Category	Theorems
withZeroUnits 📖	CompOp	2 math math: withZeroUnits_symm_apply, withZeroUnits_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
withZeroUnits_apply 📖	mathematical	—	DFunLike.coe RelIso WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Preorder.toLE WithZero.instPreorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero RelIso.instFunLike withZeroUnits WithZero.recZeroCoe MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Units.val	—	—
withZeroUnits_symm_apply 📖	mathematical	—	DFunLike.coe RelIso WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instPreorder Units.instPreorder RelIso.instFunLike RelIso.symm withZeroUnits MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass LinearOrder.toDecidableEq WithZero.instZero WithZero.coe	—	—

WithZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
withZeroUnitsEquiv_strictMono 📖	mathematical	—	StrictMono WithZero Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero instPreorder Units.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe MulEquiv MulZeroClass.toMul instMulZeroClass Units.instMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass EquivLike.toFunLike MulEquiv.instEquivLike withZeroUnitsEquiv LinearOrder.toDecidableEq MulZeroClass.toZero	—	IsOrderedMonoid.toIsOrderedCancelMonoid Units.isOrderedMonoid LinearOrderedCommMonoidWithZero.toIsOrderedMonoid
withZeroUnitsEquiv_symm_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 instPreorder Units.instPreorder DFunLike.coe MulEquiv MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass instMulZeroClass Units.instMul EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm withZeroUnitsEquiv LinearOrder.toDecidableEq MulZeroClass.toZero	—	OrderIso.strictMono

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMulPosMonoWithZeroOfMulRightMono 📖	mathematical	—	MulPosMono WithZero MulZeroClass.toMul WithZero.instMulZeroClass WithZero.instZero WithZero.instPreorder	—	MulZeroClass.mul_zero MulZeroClass.zero_mul mul_le_mul_left
instMulPosStrictMonoWithZeroOfMulRightStrictMono 📖	mathematical	—	MulPosStrictMono WithZero MulZeroClass.toMul WithZero.instMulZeroClass WithZero.instZero WithZero.instPreorder	—	WithZero.zero_lt_coe mul_lt_mul_left
instPosMulMonoWithZeroOfMulLeftMono 📖	mathematical	—	PosMulMono WithZero MulZeroClass.toMul WithZero.instMulZeroClass WithZero.instZero WithZero.instPreorder	—	MulZeroClass.zero_mul MulZeroClass.mul_zero mul_le_mul_right
instPosMulStrictMonoWithZeroOfMulLeftStrictMono 📖	mathematical	—	PosMulStrictMono WithZero MulZeroClass.toMul WithZero.instMulZeroClass WithZero.instZero WithZero.instPreorder	—	MulZeroClass.mul_zero WithZero.zero_lt_coe mul_lt_mul_right

---

← Back to Index