Defs

📁 Source: Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

Statistics

Metric	Count
Definitions `CanonicallyOrderedAdd`, `toUniqueAddUnits`, `toUniqueUnits`, `CanonicallyOrderedMul`	4
Theorems `le_add_self`, `le_self_add`, `toAddLeftMono`, `toExistsAddOfLE`, `toIsOrderedAddMonoid`, `le_mul_self`, `le_self_mul`, `toExistsMulOfLE`, `toIsOrderedMonoid`, `toMulLeftMono`, `one_lt`, `pos`, `one_lt`, `pos`, `one_lt`, `pos`, `of_ge`, `of_gt`, `of_gt'`, `pos`, `add_pos_iff`, `bot_eq_one`, `bot_eq_one'`, `bot_eq_zero`, `bot_eq_zero'`, `eq_one_or_one_lt`, `eq_zero_or_pos`, `exists_one_lt_mul_of_lt`, `exists_pos_add_of_lt`, `isBot_one`, `isBot_zero`, `le_add_left`, `le_add_of_le_left`, `le_add_of_le_right`, `le_add_right`, `le_add_self`, `le_iff_exists_add`, `le_iff_exists_add'`, `le_iff_exists_mul`, `le_iff_exists_mul'`, `le_mul_left`, `le_mul_of_le_left`, `le_mul_of_le_right`, `le_mul_right`, `le_mul_self`, `le_of_add_le_left`, `le_of_add_le_right`, `le_of_mul_le_left`, `le_of_mul_le_right`, `le_one_iff_eq_one`, `le_self_add`, `le_self_mul`, `lt_iff_exists_add`, `lt_iff_exists_mul`, `min_add_distrib`, `min_add_distrib'`, `min_mul_distrib`, `min_mul_distrib'`, `min_one`, `min_zero`, `nonpos_iff_eq_zero`, `not_lt_one`, `not_lt_zero`, `not_neg`, `one_le`, `one_lt_iff_ne_one`, `one_lt_mul_iff`, `one_lt_of_gt`, `one_lt_of_ne_one`, `one_min`, `one_notMem_iff`, `pos_iff_ne_zero`, `pos_of_gt`, `pos_of_ne_zero`, `self_le_add_left`, `self_le_add_right`, `self_le_mul_left`, `self_le_mul_right`, `zero_le`, `zero_min`, `zero_notMem_iff`	81
Total	85

CanonicallyOrderedAdd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_add_self` 📖	—	—	—	—	—
`le_self_add` 📖	—	—	—	—	—
`toAddLeftMono` 📖	mathematical	—	`AddLeftMono` `AddSemigroup.toAdd`	—	`ExistsAddOfLE.exists_add_of_le` `toExistsAddOfLE` `le_iff_exists_add` `add_assoc`
`toExistsAddOfLE` 📖	mathematical	—	`ExistsAddOfLE`	—	—
`toIsOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid`	—	`add_le_add_left` `covariant_swap_add_of_covariant_add` `toAddLeftMono`

CanonicallyOrderedCommMonoid

Definitions

Name	Category	Theorems
`toUniqueAddUnits` 📖	CompOp	—
`toUniqueUnits` 📖	CompOp	—

CanonicallyOrderedMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_mul_self` 📖	—	—	—	—	—
`le_self_mul` 📖	—	—	—	—	—
`toExistsMulOfLE` 📖	mathematical	—	`ExistsMulOfLE`	—	—
`toIsOrderedMonoid` 📖	mathematical	—	`IsOrderedMonoid`	—	`mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `toMulLeftMono`
`toMulLeftMono` 📖	mathematical	—	`MulLeftMono` `Semigroup.toMul`	—	`ExistsMulOfLE.exists_mul_of_le` `toExistsMulOfLE` `le_iff_exists_mul` `mul_assoc`

LT.lt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`one_lt` 📖	mathematical	`Preorder.toLT`	`Preorder.toLT` `MulOne.toOne` `MulOneClass.toMulOne`	—	`one_lt_of_gt`
`pos` 📖	mathematical	`Preorder.toLT`	`Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero`	—	`pos_of_gt`

NE.ne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`one_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne`	—	`Ne.one_lt`
`pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero`	—	`Ne.pos`

Ne

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`one_lt` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne`	—	`one_lt_of_ne_one`
`pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero`	—	`pos_of_ne_zero`

NeZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_ge` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder`	`AddZero.toZero` `AddZeroClass.toAddZero`	—	`of_pos` `lt_of_lt_of_le` `pos`
`of_gt` 📖	mathematical	`Preorder.toLT`	`AddZero.toZero` `AddZeroClass.toAddZero`	—	`of_pos` `pos_of_gt`
`of_gt'` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero`	—	`of_gt` `Fact.out`
`pos` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero`	—	`LE.le.lt_of_ne` `zero_le`

(root)

Definitions

Name	Category	Theorems
`CanonicallyOrderedAdd` 📖	CompData	21 math math: `ENNReal.instCanonicallyOrderedAdd`, `Finsupp.instCanonicallyOrderedAddOfAddLeftMono`, `Pi.instCanonicallyOrderedAddForall`, `Nat.instCanonicallyOrderedAdd`, `Nonneg.canonicallyOrderedAdd`, `Multiset.instCanonicallyOrderedAdd`, `Filter.Germ.instCanonicallyOrderedAdd`, `SetSemiring.instCanonicallyOrderedAdd`, `DFinsupp.instCanonicallyOrderedAddOfAddLeftMono`, `Cardinal.canonicallyOrderedAdd`, `NNRat.instCanonicallyOrderedAdd`, `LieSubalgebra.instCanonicallyOrderedAdd`, `Additive.canonicallyOrderedAdd`, `Submodule.instCanonicallyOrderedAdd`, `IdemSemiring.toCanonicallyOrderedAdd`, `Prod.instCanonicallyOrderedAdd`, `WithTop.canonicallyOrderedAdd`, `PUnit.canonicallyOrderedAdd`, `Ordinal.canonicallyOrderedAdd`, `FractionalIdeal.instCanonicallyOrderedAdd`, `WithZero.instCanonicallyOrderedAdd`
`CanonicallyOrderedMul` 📖	CompData	5 math math: `Prod.instCanonicallyOrderedMul`, `Filter.Germ.instCanonicallyOrderedMul`, `Pi.instCanonicallyOrderedMulForall`, `Multiplicative.canonicallyOrderedMul`, `Associates.instCanonicallyOrderedMul`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_pos_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddZero.toAdd`	—	`pos_iff_ne_zero` `add_eq_zero` `Unique.instSubsingleton` `not_and_or`
`bot_eq_one` 📖	mathematical	—	`Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne`	—	`IsBot.eq_bot` `isBot_one`
`bot_eq_one'` 📖	mathematical	—	`Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`bot_eq_one`
`bot_eq_zero` 📖	mathematical	—	`Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero`	—	`IsBot.eq_bot` `isBot_zero`
`bot_eq_zero'` 📖	mathematical	—	`Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`bot_eq_zero`
`eq_one_or_one_lt` 📖	mathematical	—	`MulOne.toOne` `MulOneClass.toMulOne` `Preorder.toLT` `PartialOrder.toPreorder`	—	`LE.le.eq_or_lt` `one_le`
`eq_zero_or_pos` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero` `Preorder.toLT` `PartialOrder.toPreorder`	—	`LE.le.eq_or_lt` `zero_le`
`exists_one_lt_mul_of_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`Preorder.toLT` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `MulOne.toMul`	—	`le_iff_exists_mul` `LT.lt.le` `one_lt_iff_ne_one` `mul_one`
`exists_pos_add_of_lt` 📖	mathematical	`Preorder.toLT` `PartialOrder.toPreorder`	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddZero.toAdd`	—	`le_iff_exists_add` `LT.lt.le` `pos_iff_ne_zero` `add_zero` `lt_self_iff_false`
`isBot_one` 📖	mathematical	—	`IsBot` `MulOne.toOne` `MulOneClass.toMulOne`	—	`one_le`
`isBot_zero` 📖	mathematical	—	`IsBot` `AddZero.toZero` `AddZeroClass.toAddZero`	—	`zero_le`
`le_add_left` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE`	—	`le_add_of_le_right`
`le_add_of_le_left` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE`	—	`LE.le.trans'` `le_self_add`
`le_add_of_le_right` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE`	—	`LE.le.trans'` `le_add_self`
`le_add_right` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE`	—	`le_add_of_le_left`
`le_add_self` 📖	—	—	—	—	`CanonicallyOrderedAdd.le_add_self`
`le_iff_exists_add` 📖	—	—	—	—	`ExistsAddOfLE.exists_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `le_self_add`
`le_iff_exists_add'` 📖	mathematical	—	`Preorder.toLE` `AddCommMagma.toAdd`	—	`le_iff_exists_add` `add_comm`
`le_iff_exists_mul` 📖	—	—	—	—	`ExistsMulOfLE.exists_mul_of_le` `CanonicallyOrderedMul.toExistsMulOfLE` `le_self_mul`
`le_iff_exists_mul'` 📖	mathematical	—	`Preorder.toLE` `CommMagma.toMul`	—	`mul_comm`
`le_mul_left` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE`	—	`le_mul_of_le_right`
`le_mul_of_le_left` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE`	—	`LE.le.trans'` `le_self_mul`
`le_mul_of_le_right` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE`	—	`LE.le.trans'` `le_mul_self`
`le_mul_right` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE`	—	`le_mul_of_le_left`
`le_mul_self` 📖	—	—	—	—	`CanonicallyOrderedMul.le_mul_self`
`le_of_add_le_left` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE`	—	`LE.le.trans` `le_self_add`
`le_of_add_le_right` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE`	—	`LE.le.trans` `le_add_self`
`le_of_mul_le_left` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE`	—	`LE.le.trans` `le_self_mul`
`le_of_mul_le_right` 📖	mathematical	`Preorder.toLE`	`Preorder.toLE`	—	`LE.le.trans` `le_mul_self`
`le_one_iff_eq_one` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne`	—	`LE.le.ge_iff_eq'` `one_le`
`le_self_add` 📖	—	—	—	—	`CanonicallyOrderedAdd.le_self_add`
`le_self_mul` 📖	—	—	—	—	`CanonicallyOrderedMul.le_self_mul`
`lt_iff_exists_add` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddZero.toAdd`	—	`lt_iff_le_and_ne` `le_iff_exists_add` `pos_iff_ne_zero` `add_zero` `LE.le.lt_iff_ne` `self_le_add_right` `lt_add_of_pos_right`
`lt_iff_exists_mul` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `MulOne.toMul`	—	`lt_iff_le_and_ne` `le_iff_exists_mul` `one_lt_iff_ne_one` `mul_one` `LE.le.lt_iff_ne` `self_le_mul_right` `lt_mul_of_one_lt_right'`
`min_add_distrib` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`le_total` `inf_of_le_left` `le_add_right` `self_le_add_right` `le_add_left` `self_le_add_left` `inf_of_le_right`
`min_add_distrib'` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`min_comm` `min_add_distrib`
`min_mul_distrib` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`le_total` `inf_of_le_left` `inf_of_le_right`
`min_mul_distrib'` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`min_comm` `min_mul_distrib`
`min_one` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`min_eq_right` `one_le`
`min_zero` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`min_eq_right` `zero_le`
`nonpos_iff_eq_zero` 📖	mathematical	—	`Preorder.toLE` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero`	—	`LE.le.ge_iff_eq'` `zero_le`
`not_lt_one` 📖	mathematical	—	`Preorder.toLT` `MulOne.toOne` `MulOneClass.toMulOne`	—	`LE.le.not_gt` `one_le`
`not_lt_zero` 📖	mathematical	—	`Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero`	—	`LE.le.not_gt` `zero_le`
`not_neg` 📖	mathematical	—	`Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero`	—	`not_lt_zero`
`one_le` 📖	mathematical	—	`MulOne.toOne` `MulOneClass.toMulOne`	—	`LE.le.trans_eq` `le_self_mul` `one_mul`
`one_lt_iff_ne_one` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne`	—	`LE.le.lt_iff_ne` `one_le`
`one_lt_mul_iff` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `MulOne.toMul`	—	`Unique.instSubsingleton`
`one_lt_of_gt` 📖	mathematical	`Preorder.toLT`	`Preorder.toLT` `MulOne.toOne` `MulOneClass.toMulOne`	—	`LE.le.trans_lt` `one_le`
`one_lt_of_ne_one` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `MulOne.toOne` `MulOneClass.toMulOne`	—	`one_lt_iff_ne_one`
`one_min` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`min_eq_left` `one_le`
`one_notMem_iff` 📖	mathematical	—	`Set` `Set.instMembership` `MulOne.toOne` `MulOneClass.toMulOne` `Preorder.toLT` `PartialOrder.toPreorder`	—	`bot_notMem_iff` `bot_eq_one`
`pos_iff_ne_zero` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero`	—	`LE.le.lt_iff_ne` `zero_le`
`pos_of_gt` 📖	mathematical	`Preorder.toLT`	`Preorder.toLT` `AddZero.toZero` `AddZeroClass.toAddZero`	—	`LE.le.trans_lt` `zero_le`
`pos_of_ne_zero` 📖	mathematical	—	`Preorder.toLT` `PartialOrder.toPreorder` `AddZero.toZero` `AddZeroClass.toAddZero`	—	`pos_iff_ne_zero`
`self_le_add_left` 📖	—	—	—	—	`le_add_self`
`self_le_add_right` 📖	—	—	—	—	`le_self_add`
`self_le_mul_left` 📖	—	—	—	—	`le_mul_self`
`self_le_mul_right` 📖	—	—	—	—	`le_self_mul`
`zero_le` 📖	mathematical	—	`AddZero.toZero` `AddZeroClass.toAddZero`	—	`LE.le.trans_eq` `le_self_add` `zero_add`
`zero_min` 📖	mathematical	—	`SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`min_eq_left` `zero_le`
`zero_notMem_iff` 📖	mathematical	—	`Set` `Set.instMembership` `AddZero.toZero` `AddZeroClass.toAddZero` `Preorder.toLT` `PartialOrder.toPreorder`	—	`bot_notMem_iff` `bot_eq_zero`

---

← Back to Index