Defs

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

Statistics

Metric	Count
Definitions IsOrderedAddMonoid, IsOrderedCancelAddMonoid, IsOrderedCancelMonoid, IsOrderedMonoid	4
Theorems add_le_add_left, add_le_add_right, toAddLeftMono, toAddRightMono, le_of_add_le_add_left, le_of_add_le_add_right, of_add_lt_add_left, toAddLeftReflectLE, toAddLeftReflectLT, toAddRightReflectLT, toIsCancelAdd, toIsOrderedAddMonoid, le_of_mul_le_mul_left, le_of_mul_le_mul_right, of_mul_lt_mul_left, toIsCancelMul, toIsOrderedMonoid, toMulLeftReflectLE, toMulLeftReflectLT, toMulRightReflectLT, mul_le_mul_left, mul_le_mul_right, toMulLeftMono, toMulRightMono, add_self_neg_iff, add_self_nonpos_iff, mul_self_le_one_iff, mul_self_lt_one_iff, nonneg_add_self_iff, one_le_mul_self_iff, one_lt_mul_self_iff, pos_add_self_iff	32
Total	36

IsOrderedAddMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_le_add_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
add_le_add_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
toAddLeftMono 📖	mathematical	—	AddLeftMono AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Preorder.toLE PartialOrder.toPreorder	—	add_le_add_right
toAddRightMono 📖	mathematical	—	AddRightMono AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Preorder.toLE PartialOrder.toPreorder	—	add_le_add_left

IsOrderedCancelAddMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_of_add_le_add_left 📖	—	Preorder.toLE PartialOrder.toPreorder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—	—
le_of_add_le_add_right 📖	—	Preorder.toLE PartialOrder.toPreorder AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—	—
of_add_lt_add_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	IsOrderedCancelAddMonoid	—	eq_or_lt_of_le le_refl add_comm LT.lt.le Mathlib.Tactic.Contrapose.contrapose₁ not_le
toAddLeftReflectLE 📖	mathematical	—	AddLeftReflectLE AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Preorder.toLE PartialOrder.toPreorder	—	le_of_add_le_add_left
toAddLeftReflectLT 📖	mathematical	—	AddLeftReflectLT AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Preorder.toLT PartialOrder.toPreorder	—	contravariant_lt_of_contravariant_le ContravariantClass.elim toAddLeftReflectLE
toAddRightReflectLT 📖	mathematical	—	AddRightReflectLT AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Preorder.toLT PartialOrder.toPreorder	—	contravariant_swap_add_of_contravariant_add toAddLeftReflectLT
toIsCancelAdd 📖	mathematical	—	IsCancelAdd AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	LE.le.antisymm le_of_add_le_add_left toAddLeftReflectLE Eq.le Eq.ge le_of_add_le_add_right contravariant_swap_add_of_contravariant_add
toIsOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid	—	—

IsOrderedCancelMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_of_mul_le_mul_left 📖	—	Preorder.toLE PartialOrder.toPreorder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	—	—
le_of_mul_le_mul_right 📖	—	Preorder.toLE PartialOrder.toPreorder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	—	—
of_mul_lt_mul_left 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	IsOrderedCancelMonoid	—	eq_or_lt_of_le mul_comm LT.lt.le Mathlib.Tactic.Contrapose.contrapose₁
toIsCancelMul 📖	mathematical	—	IsCancelMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	LE.le.antisymm le_of_mul_le_mul_left' toMulLeftReflectLE Eq.le Eq.ge le_of_mul_le_mul_right' contravariant_swap_mul_of_contravariant_mul
toIsOrderedMonoid 📖	mathematical	—	IsOrderedMonoid	—	—
toMulLeftReflectLE 📖	mathematical	—	MulLeftReflectLE MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Preorder.toLE PartialOrder.toPreorder	—	le_of_mul_le_mul_left
toMulLeftReflectLT 📖	mathematical	—	MulLeftReflectLT MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Preorder.toLT PartialOrder.toPreorder	—	contravariant_lt_of_contravariant_le ContravariantClass.elim toMulLeftReflectLE
toMulRightReflectLT 📖	mathematical	—	MulRightReflectLT MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Preorder.toLT PartialOrder.toPreorder	—	contravariant_swap_mul_of_contravariant_mul toMulLeftReflectLT

IsOrderedMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_le_mul_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	—
mul_le_mul_right 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid	—	—
toMulLeftMono 📖	mathematical	—	MulLeftMono MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Preorder.toLE PartialOrder.toPreorder	—	mul_le_mul_right
toMulRightMono 📖	mathematical	—	MulRightMono MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid Preorder.toLE PartialOrder.toPreorder	—	mul_le_mul_left

(root)

Definitions

Name	Category	Theorems
IsOrderedAddMonoid 📖	CompData	51 math math: Submodule.toIsOrderedAddMonoid, MeasureTheory.Lp.instIsOrderedAddMonoid, Finsupp.isOrderedAddMonoid, MeasureTheory.Measure.instIsOrderedAddMonoid, Nat.instIsOrderedAddMonoid, MeasureTheory.SimpleFunc.instIsOrderedAddMonoid, Prod.Lex.isOrderedAddMonoid, WithZero.isOrderedAddMonoid, Filter.Germ.instIsOrderedAddMonoid, BoundedContinuousFunction.instIsOrderedAddMonoid, ArchimedeanClass.instIsOrderedAddMonoid, LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid, ZNum.isOrderedAddMonoid, Function.locallyFinsuppWithin.instIsOrderedAddMonoid, Rat.instIsOrderedAddMonoid, CanonicallyOrderedAdd.toIsOrderedAddMonoid, ContinuousMap.instIsOrderedAddMonoid, AddSubgroup.toIsOrderedAddMonoid, PartENat.isOrderedAddMonoid, WithTop.isOrderedAddMonoid, LinearOrderedAddCommGroupWithTop.toIsOrderedAddMonoid, AddOpposite.instIsOrderedAddMonoid, CompactlySupportedContinuousMap.instIsOrderedAddMonoid, SetTheory.Game.isOrderedAddMonoid, MulOpposite.instIsOrderedAddMonoid, RCLike.toIsOrderedAddMonoid, WithBot.isOrderedAddMonoid, AddSubmonoidClass.toIsOrderedAddMonoid, Matrix.instIsOrderedAddMonoid, AddSubmonoid.toIsOrderedAddMonoid, HahnSeries.instIsOrderedAddMonoidLex, Zsqrtd.instIsOrderedAddMonoidCastInt, Nonneg.isOrderedAddMonoid, LieSubalgebra.instIsOrderedAddMonoid, IsOrderedRing.toIsOrderedAddMonoid, MeasureTheory.OuterMeasure.instIsOrderedAddMonoid, Surreal.isOrderedAddMonoid, StrictMono.isOrderedAddMonoid, instIsOrderedAddMonoidEReal, AddUnits.isOrderedAddMonoid, Real.instIsOrderedAddMonoid, ENNReal.instIsOrderedAddMonoid, Submodule.instIsOrderedAddMonoid, OrderDual.isOrderedAddMonoid, StarOrderedRing.toIsOrderedAddMonoid, Prod.instIsOrderedAddMonoid, IsOrderedCancelAddMonoid.toIsOrderedAddMonoid, IdemSemiring.toIsOrderedAddMonoid, Additive.isOrderedAddMonoid, Int.instIsOrderedAddMonoid, Function.Injective.isOrderedAddMonoid
IsOrderedCancelAddMonoid 📖	CompData	30 math math: AddSubmonoid.toIsOrderedCancelAddMonoid, instIsOrderedCancelAddMonoidLexFinsupp, AddLocalization.isOrderedAddCancelMonoid, Finsupp.Colex.isOrderedCancelAddMonoid, Multiset.instIsOrderedCancelAddMonoid, Finsupp.isOrderedCancelAddMonoid, ConditionallyCompleteLinearOrderedField.toIsOrderedCancelAddMonoid, NatOrdinal.instIsOrderedCancelAddMonoid, PUnit.isOrderedCancelAddMonoid, AddSubmonoidClass.toIsOrderedCancelAddMonoid, IsStrictOrderedRing.toIsOrderedCancelAddMonoid, IsOrderedAddMonoid.toIsOrderedCancelAddMonoid, Additive.isOrderedCancelAddMonoid, IsOrderedCancelAddMonoid.of_add_lt_add_left, DivisibleHull.instIsOrderedCancelAddMonoid, Function.Injective.isOrderedCancelAddMonoid, Prod.instIsOrderedAddCancelMonoid, Nat.instIsOrderedCancelAddMonoid, OrderDual.isOrderedAddCancelMonoid, Submodule.toIsOrderedCancelAddMonoid, Finsupp.Lex.isOrderedCancelAddMonoid, Seminorm.instIsOrderedCancelAddMonoid, Finsupp.DegLex.instIsOrderedCancelAddMonoidDegLexNat, Filter.Germ.instIsOrderedAddCancelMonoid, StrictMono.isOrderedAddCancelMonoid, Num.isOrderedCancelAddMonoid, MonomialOrder.iocam, Nonneg.isOrderedCancelAddMonoid, Prod.Lex.isOrderedAddCancelMonoid, Real.instIsOrderedCancelAddMonoid
IsOrderedCancelMonoid 📖	CompData	14 math math: IsOrderedCancelMonoid.of_mul_lt_mul_left, IsOrderedMonoid.toIsOrderedCancelMonoid, PNat.instIsOrderedCancelMonoid, StrictMono.isOrderedCancelMonoid, Localization.isOrderedCancelMonoid, Function.Injective.isOrderedCancelMonoid, Filter.Germ.instIsOrderedCancelMonoid, Multiplicative.isOrderedCancelMonoid, Prod.instIsOrderedCancelMonoid, SubmonoidClass.toIsOrderedCancelMonoid, Positive.isOrderedCancelMonoid, Prod.Lex.isOrderedCancelMonoid, Submonoid.toIsOrderedCancelMonoid, OrderDual.isOrderedCancelMonoid
IsOrderedMonoid 📖	CompData	25 math math: WithZero.isOrderedMonoid, SubmonoidClass.toIsOrderedMonoid, CanonicallyOrderedMul.toIsOrderedMonoid, Prod.instIsOrderedMonoid, NatOrdinal.instIsOrderedMonoid, StrictMono.isOrderedMonoid, Associates.instIsOrderedMonoid, ENNReal.instIsOrderedMonoid, LinearOrderedCommMonoidWithZero.toIsOrderedMonoid, MulOpposite.instIsOrderedMonoid, Positive.isOrderedMonoid, ValuativeRel.instIsOrderedMonoidValueGroupWithZero, IsOrderedCancelMonoid.toIsOrderedMonoid, Submonoid.toIsOrderedMonoid, Subgroup.toIsOrderedMonoid, Multiplicative.isOrderedMonoid, ContinuousMap.instIsOrderedMonoid, Function.Injective.isOrderedMonoid, Prod.Lex.isOrderedMonoid, Units.isOrderedMonoid, CanonicallyOrderedAdd.toIsOrderedMonoid, OrderDual.isOrderedMonoid, MeasureTheory.SimpleFunc.instIsOrderedMonoid, AddOpposite.instIsOrderedMonoid, Filter.Germ.instIsOrderedMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_self_neg_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddZero.toZero	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ not_lt nonneg_add_self_iff
add_self_nonpos_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddZero.toZero	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ not_le pos_add_self_iff
mul_self_le_one_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MulOne.toOne	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ one_lt_mul_self_iff
mul_self_lt_one_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MulOne.toOne	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ one_le_mul_self_iff
nonneg_add_self_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddZero.toAdd	—	Function.mtr not_le add_neg' IsOrderedAddMonoid.toAddLeftMono add_nonneg
one_le_mul_self_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MulOne.toMul	—	Function.mtr mul_lt_one' IsOrderedMonoid.toMulLeftMono one_le_mul
one_lt_mul_self_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid MulOne.toMul	—	Function.mtr mul_le_one' IsOrderedMonoid.toMulLeftMono one_lt_mul''
pos_add_self_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddZero.toAdd	—	Function.mtr not_lt add_nonpos IsOrderedAddMonoid.toAddLeftMono add_pos'

---

← Back to Index