Documentation

Mathlib.Algebra.Order.Group.Defs

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 α :

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

@[deprecated "Use `[CommGroup α] [PartialOrder α] [IsOrderedMonoid α]` instead." (since := "2025-04-10")]
structure OrderedCommGroup (α : Type u) extends CommGroup α, PartialOrder α :

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

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

Linearly ordered commutative groups #

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

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

@[deprecated "Use `[CommGroup α] [LinearOrder α] [IsOrderedMonoid α]` instead." (since := "2025-04-10")]
structure LinearOrderedCommGroup (α : Type u) extends OrderedCommGroup α, LinearOrder α :

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

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
@[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 bb⁻¹ 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 < bb⁻¹ < 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 < aa⁻¹ < 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 aa⁻¹ 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 11 a⁻¹
theorem neg_nonneg_of_nonpos {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a : α} :
a 00 -a