Defs

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

Statistics

Metric	Count
Definitions	0
Theorems toIsOrderedCancelAddMonoid, toIsOrderedCancelMonoid, to_noMaxOrder, to_noMinOrder, mul_lt_mul_left', mul_lt_mul_right', to_noMaxOrder, to_noMinOrder, add_lt_add_left', le_of_add_le_add_left, le_of_mul_le_mul_left, lt_of_add_lt_add_left, lt_of_mul_lt_mul_left, mul_lt_mul_left', eq_one_of_inv_eq', eq_zero_of_neg_eq, exists_one_lt', exists_zero_lt, inv_le_inv', inv_le_one_of_one_le, inv_le_self_iff, inv_lt_inv', inv_lt_one_of_one_lt, inv_lt_self_iff, le_inv_self_iff, le_neg_self_iff, lt_inv_self_iff, lt_neg_self_iff, neg_le_neg, neg_le_self_iff, neg_lt_neg, neg_lt_self_iff, neg_neg_of_pos, neg_nonneg_of_nonpos, neg_nonpos_of_nonneg, one_le_inv_of_le_one	36
Total	36

IsOrderedAddMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsOrderedCancelAddMonoid 📖	mathematical	—	IsOrderedCancelAddMonoid AddCommGroup.toAddCommMonoid	—	neg_add_cancel_left add_le_add_right toAddLeftMono neg_add_cancel_comm_assoc

IsOrderedMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsOrderedCancelMonoid 📖	mathematical	—	IsOrderedCancelMonoid CommGroup.toCommMonoid	—	inv_mul_cancel_left mul_le_mul_right toMulLeftMono inv_mul_cancel_comm_assoc

LinearOrderedAddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_noMaxOrder 📖	mathematical	—	NoMaxOrder Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	exists_zero_lt lt_add_of_pos_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono
to_noMinOrder 📖	mathematical	—	NoMinOrder Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	exists_zero_lt sub_lt_self_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono

LinearOrderedCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_lt_mul_left' 📖	—	—	—	—	mul_lt_mul_right
mul_lt_mul_right' 📖	—	—	—	—	mul_lt_mul_left
to_noMaxOrder 📖	mathematical	—	NoMaxOrder Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	exists_one_lt' lt_mul_of_one_lt_right' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono
to_noMinOrder 📖	mathematical	—	NoMinOrder Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	exists_one_lt' div_lt_self_iff IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono

OrderedAddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_lt_add_left' 📖	—	—	—	—	add_lt_add_right

OrderedCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
le_of_add_le_add_left 📖	—	—	—	—	le_of_add_le_add_left
le_of_mul_le_mul_left 📖	—	—	—	—	le_of_mul_le_mul_left'
lt_of_add_lt_add_left 📖	—	—	—	—	lt_of_add_lt_add_left
lt_of_mul_lt_mul_left 📖	—	—	—	—	lt_of_mul_lt_mul_left'
mul_lt_mul_left' 📖	—	—	—	—	mul_lt_mul_right

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_one_of_inv_eq' 📖	mathematical	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	InvOneClass.toOne	—	lt_trichotomy one_lt_inv_of_inv IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono LT.lt.asymm inv_lt_one'
eq_zero_of_neg_eq 📖	mathematical	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	NegZeroClass.toZero	—	lt_trichotomy neg_pos_of_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono LT.lt.asymm neg_lt_zero
exists_one_lt' 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	Decidable.exists_ne Ne.lt_or_gt one_lt_inv' IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono
exists_zero_lt 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Decidable.exists_ne Ne.lt_or_gt neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono
inv_le_inv' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	inv_le_inv_iff IsOrderedMonoid.toMulLeftMono covariant_swap_mul_of_covariant_mul
inv_le_one_of_one_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	InvOneClass.toInv	—	inv_le_one' IsOrderedMonoid.toMulLeftMono
inv_le_self_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid InvOneClass.toOne	—	IsOrderedMonoid.toMulLeftMono
inv_lt_inv' 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	inv_lt_inv_iff IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono IsRightCancelMul.mulRightStrictMono_of_mulRightMono RightCancelSemigroup.toIsRightCancelMul covariant_swap_mul_of_covariant_mul
inv_lt_one_of_one_lt 📖	mathematical	Preorder.toLT PartialOrder.toPreorder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	InvOneClass.toInv	—	inv_lt_one_iff_one_lt IsLeftCancelMul.mulLeftStrictMono_of_mulLeftMono LeftCancelSemigroup.toIsLeftCancelMul IsOrderedMonoid.toMulLeftMono
inv_lt_self_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid InvOneClass.toOne	—	IsRightCancelMul.mulRightStrictMono_of_mulRightMono RightCancelSemigroup.toIsRightCancelMul covariant_swap_mul_of_covariant_mul IsOrderedMonoid.toMulLeftMono
le_inv_self_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid InvOneClass.toOne	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ inv_lt_self_iff
le_neg_self_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NegZeroClass.toZero	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ not_le neg_lt_self_iff
lt_inv_self_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid InvOneClass.toOne	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ inv_le_self_iff
lt_neg_self_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NegZeroClass.toZero	—	Mathlib.Tactic.Contrapose.contrapose_iff₁ not_lt neg_le_self_iff
neg_le_neg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	neg_le_neg_iff IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add
neg_le_self_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NegZeroClass.toZero	—	neg_le_iff_add_nonneg' IsOrderedAddMonoid.toAddLeftMono nonneg_add_self_iff
neg_lt_neg 📖	mathematical	Preorder.toLT PartialOrder.toPreorder	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	neg_lt_neg_iff IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add
neg_lt_self_iff 📖	mathematical	—	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NegZeroClass.toZero	—	neg_lt_iff_pos_add IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono pos_add_self_iff
neg_neg_of_pos 📖	mathematical	Preorder.toLT PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	NegZeroClass.toNeg	—	neg_neg_iff_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono
neg_nonneg_of_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	NegZeroClass.toNeg	—	neg_nonneg IsOrderedAddMonoid.toAddLeftMono
neg_nonpos_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	NegZeroClass.toNeg	—	neg_nonpos IsOrderedAddMonoid.toAddLeftMono
one_le_inv_of_le_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	InvOneClass.toInv	—	one_le_inv' IsOrderedMonoid.toMulLeftMono

---

← Back to Index