Ordered groups

This file defines bundled ordered groups and develops a few basic results.

Implementation details

Unfortunately, the number of ' appended to lemmas in this file may differ between the multiplicative and the additive version of a lemma. The reason is that we did not want to change existing names in the library.

@[deprecated "Use `[AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α]` instead." (since := "2025-04-10")]

structure OrderedAddCommGroup (α : Type u) extends AddCommGroup α, PartialOrder α : Type u

An ordered additive commutative group is an additive commutative group with a partial order in which addition is strictly monotone.

• add : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero : α
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (a : α) : -a + a = 0
• add_comm (a b : α) : a + b = b + a
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b

  Addition is monotone in an ordered additive commutative group.

@[deprecated "Use `[CommGroup α] [PartialOrder α] [IsOrderedMonoid α]` instead." (since := "2025-04-10")]

structure OrderedCommGroup (α : Type u) extends CommGroup α, PartialOrder α : Type u

An ordered commutative group is a commutative group with a partial order in which multiplication is strictly monotone.

• mul : α → α → α
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• one : α
• one_mul (a : α) : 1 * a = a
• mul_one (a : α) : a * 1 = a
• npow : ℕ → α → α
• npow_zero (x : α) : Monoid.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Monoid.npow (n + 1) x = Monoid.npow n x * x
• inv : α → α
• div : α → α → α
• div_eq_mul_inv (a b : α) : a / b = a * b⁻¹
• zpow : ℤ → α → α
• zpow_zero' (a : α) : DivInvMonoid.zpow 0 a = 1
• zpow_succ' (n : ℕ) (a : α) : DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
• zpow_neg' (n : ℕ) (a : α) : DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
• inv_mul_cancel (a : α) : a⁻¹ * a = 1
• mul_comm (a b : α) : a * b = b * a
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• mul_le_mul_left (a b : α) : a ≤ b → ∀ (c : α), c * a ≤ c * b

  Multiplication is monotone in an ordered commutative group.

theorem OrderedCommGroup.mul_lt_mul_left' {α : Type u_1} [Mul α] [LT α] [MulLeftStrictMono α] {b c : α} (bc : b < c) (a : α) : a * b < a * c

Alias of mul_lt_mul_left'.

theorem OrderedAddCommGroup.add_lt_add_left {α : Type u_1} [Add α] [LT α] [AddLeftStrictMono α] {b c : α} (bc : b < c) (a : α) : a + b < a + c

theorem OrderedCommGroup.le_of_mul_le_mul_left {α : Type u_1} [Mul α] [LE α] [MulLeftReflectLE α] {a b c : α} (bc : a * b ≤ a * c) : b ≤ c

Alias of le_of_mul_le_mul_left'.

theorem OrderedAddCommGroup.le_of_add_le_add_left {α : Type u_1} [Add α] [LE α] [AddLeftReflectLE α] {a b c : α} (bc : a + b ≤ a + c) : b ≤ c

theorem OrderedCommGroup.lt_of_mul_lt_mul_left {α : Type u_1} [Mul α] [LT α] [MulLeftReflectLT α] {a b c : α} (bc : a * b < a * c) : b < c

Alias of lt_of_mul_lt_mul_left'.

theorem OrderedAddCommGroup.lt_of_add_lt_add_left {α : Type u_1} [Add α] [LT α] [AddLeftReflectLT α] {a b c : α} (bc : a + b < a + c) : b < c

@[instance 100]

instance IsOrderedMonoid.toIsOrderedCancelMonoid {α : Type u} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] : IsOrderedCancelMonoid α

@[instance 100]

instance IsOrderedAddMonoid.toIsOrderedCancelAddMonoid {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] : IsOrderedCancelAddMonoid α

Linearly ordered commutative groups

@[deprecated "Use `[AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α]` instead." (since := "2025-04-10")]

structure LinearOrderedAddCommGroup (α : Type u) extends OrderedAddCommGroup α, LinearOrder α : Type u

A linearly ordered additive commutative group is an additive commutative group with a linear order in which addition is monotone.

• add : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• zero : α
• zero_add (a : α) : 0 + a = a
• add_zero (a : α) : a + 0 = a
• nsmul : ℕ → α → α
• nsmul_zero (x : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n x + x
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg (a b : α) : a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' (a : α) : SubNegMonoid.zsmul 0 a = 0
• zsmul_succ' (n : ℕ) (a : α) : SubNegMonoid.zsmul (↑n.succ) a = SubNegMonoid.zsmul (↑n) a + a
• zsmul_neg' (n : ℕ) (a : α) : SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑n.succ) a
• neg_add_cancel (a : α) : -a + a = 0
• add_comm (a b : α) : a + b = b + a
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• add_le_add_left (a b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE α
• toDecidableEq : DecidableEq α
• toDecidableLT : DecidableLT α
• min_def (a b : α) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : α) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b

@[deprecated "Use `[CommGroup α] [LinearOrder α] [IsOrderedMonoid α]` instead." (since := "2025-04-10")]

structure LinearOrderedCommGroup (α : Type u) extends OrderedCommGroup α, LinearOrder α : Type u

A linearly ordered commutative group is a commutative group with a linear order in which multiplication is monotone.

• mul : α → α → α
• mul_assoc (a b c : α) : a * b * c = a * (b * c)
• one : α
• one_mul (a : α) : 1 * a = a
• mul_one (a : α) : a * 1 = a
• npow : ℕ → α → α
• npow_zero (x : α) : Monoid.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Monoid.npow (n + 1) x = Monoid.npow n x * x
• inv : α → α
• div : α → α → α
• div_eq_mul_inv (a b : α) : a / b = a * b⁻¹
• zpow : ℤ → α → α
• zpow_zero' (a : α) : DivInvMonoid.zpow 0 a = 1
• zpow_succ' (n : ℕ) (a : α) : DivInvMonoid.zpow (↑n.succ) a = DivInvMonoid.zpow (↑n) a * a
• zpow_neg' (n : ℕ) (a : α) : DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
• inv_mul_cancel (a : α) : a⁻¹ * a = 1
• mul_comm (a b : α) : a * b = b * a
• le : α → α → Prop
• lt : α → α → Prop
• le_refl (a : α) : a ≤ a
• le_trans (a b c : α) : a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm (a b : α) : a ≤ b → b ≤ a → a = b
• mul_le_mul_left (a b : α) : a ≤ b → ∀ (c : α), c * a ≤ c * b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE α
• toDecidableEq : DecidableEq α
• toDecidableLT : DecidableLT α
• min_def (a b : α) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : α) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b

theorem LinearOrderedCommGroup.mul_lt_mul_left' {α : Type u} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] (a b : α) (h : a < b) (c : α) : c * a < c * b

theorem LinearOrderedAddCommGroup.add_lt_add_left {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] (a b : α) (h : a < b) (c : α) : c + a < c + b

theorem eq_one_of_inv_eq' {α : Type u} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] {a : α} (h : a⁻¹ = a) : a = 1

theorem eq_zero_of_neg_eq {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} (h : -a = a) : a = 0

theorem exists_one_lt' {α : Type u} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [Nontrivial α] : ∃ (a : α), 1 < a

theorem exists_zero_lt {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Nontrivial α] : ∃ (a : α), 0 < a

@[instance 100]

instance LinearOrderedCommGroup.to_noMaxOrder {α : Type u} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [Nontrivial α] : NoMaxOrder α

@[instance 100]

instance LinearOrderedAddCommGroup.to_noMaxOrder {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Nontrivial α] : NoMaxOrder α

@[instance 100]

instance LinearOrderedCommGroup.to_noMinOrder {α : Type u} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [Nontrivial α] : NoMinOrder α

@[instance 100]

instance LinearOrderedAddCommGroup.to_noMinOrder {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Nontrivial α] : NoMinOrder α

@[simp]

theorem inv_le_self_iff {α : Type u} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] {a : α} : a⁻¹ ≤ a ↔ 1 ≤ a

@[simp]

theorem neg_le_self_iff {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} : -a ≤ a ↔ 0 ≤ a

@[simp]

theorem inv_lt_self_iff {α : Type u} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] {a : α} : a⁻¹ < a ↔ 1 < a

@[simp]

theorem neg_lt_self_iff {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} : -a < a ↔ 0 < a

@[simp]

theorem le_inv_self_iff {α : Type u} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] {a : α} : a ≤ a⁻¹ ↔ a ≤ 1

@[simp]

theorem le_neg_self_iff {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} : a ≤ -a ↔ a ≤ 0

@[simp]

theorem lt_inv_self_iff {α : Type u} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] {a : α} : a < a⁻¹ ↔ a < 1

@[simp]

theorem lt_neg_self_iff {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} : a < -a ↔ a < 0

theorem inv_le_inv' {α : Type u} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {a b : α} : a ≤ b → b⁻¹ ≤ a⁻¹

theorem neg_le_neg {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b : α} : a ≤ b → -b ≤ -a

theorem inv_lt_inv' {α : Type u} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {a b : α} : a < b → b⁻¹ < a⁻¹

theorem neg_lt_neg {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b : α} : a < b → -b < -a

theorem inv_lt_one_of_one_lt {α : Type u} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {a : α} : 1 < a → a⁻¹ < 1

theorem neg_neg_of_pos {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a : α} : 0 < a → -a < 0

theorem inv_le_one_of_one_le {α : Type u} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {a : α} : 1 ≤ a → a⁻¹ ≤ 1

theorem neg_nonpos_of_nonneg {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a : α} : 0 ≤ a → -a ≤ 0

theorem one_le_inv_of_le_one {α : Type u} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {a : α} : a ≤ 1 → 1 ≤ a⁻¹

theorem neg_nonneg_of_nonpos {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a : α} : a ≤ 0 → 0 ≤ -a