# 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.

class OrderedAddCommGroup (α : Type u) extends , :

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 : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), SubNegMonoid.zsmul (Int.ofNat n.succ) a = + a
• zsmul_neg' : ∀ (n : ) (a : α), = -SubNegMonoid.zsmul (↑n.succ) a
• add_left_neg : ∀ (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 bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b

Addition is monotone in an ordered additive commutative group.

Instances
theorem OrderedAddCommGroup.add_le_add_left {α : Type u} [self : ] (a : α) (b : α) :
a b∀ (c : α), c + a c + b

Addition is monotone in an ordered additive commutative group.

class OrderedCommGroup (α : Type u) extends , :

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 : α), = 1
• npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = * x
• inv : αα
• div : ααα
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹
• zpow : αα
• zpow_zero' : ∀ (a : α), = 1
• zpow_succ' : ∀ (n : ) (a : α), DivInvMonoid.zpow (Int.ofNat n.succ) a = * a
• zpow_neg' : ∀ (n : ) (a : α), = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
• mul_left_inv : ∀ (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 bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b

Multiplication is monotone in an ordered commutative group.

Instances
theorem OrderedCommGroup.mul_le_mul_left {α : Type u} [self : ] (a : α) (b : α) :
a b∀ (c : α), c * a c * b

Multiplication is monotone in an ordered commutative group.

instance OrderedAddCommGroup.to_covariantClass_left_le (α : Type u) :
CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1
Equations
• =
instance OrderedCommGroup.to_covariantClass_left_le (α : Type u) [] :
CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1
Equations
• =
@[instance 100]
Equations
• OrderedAddCommGroup.toOrderedCancelAddCommMonoid = let __src := inst;
theorem OrderedAddCommGroup.toOrderedCancelAddCommMonoid.proof_2 {α : Type u_1} (a : α) (b : α) (c : α) (bc : a + b a + c) :
b c
theorem OrderedAddCommGroup.toOrderedCancelAddCommMonoid.proof_1 {α : Type u_1} (a : α) (b : α) :
a + b = b + a
@[instance 100]
Equations
• OrderedCommGroup.toOrderedCancelCommMonoid = let __src := inst;
theorem OrderedAddCommGroup.to_contravariantClass_left_le (α : Type u) :
ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1

A choice-free shortcut instance.

theorem OrderedCommGroup.to_contravariantClass_left_le (α : Type u) [] :
ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1

A choice-free shortcut instance.

theorem OrderedAddCommGroup.to_contravariantClass_right_le (α : Type u) :
ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1

A choice-free shortcut instance.

theorem OrderedCommGroup.to_contravariantClass_right_le (α : Type u) [] :
ContravariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1

A choice-free shortcut instance.

theorem OrderedCommGroup.mul_lt_mul_left' {α : Type u_1} [Mul α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] {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 α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] {b : α} {c : α} (bc : b < c) (a : α) :
a + b < a + c
theorem OrderedCommGroup.le_of_mul_le_mul_left {α : Type u_1} [Mul α] [LE α] [ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {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 α] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {a : α} {b : α} {c : α} (bc : a + b a + c) :
b c
theorem OrderedCommGroup.lt_of_mul_lt_mul_left {α : Type u_1} [Mul α] [LT α] [ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] {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 α] [ContravariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] {a : α} {b : α} {c : α} (bc : a + b < a + c) :
b < c

### Linearly ordered commutative groups #

class LinearOrderedAddCommGroup (α : Type u) extends , , , :

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 : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = + x
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), SubNegMonoid.zsmul (Int.ofNat n.succ) a = + a
• zsmul_neg' : ∀ (n : ) (a : α), = -SubNegMonoid.zsmul (↑n.succ) a
• add_left_neg : ∀ (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 bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = 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

A linear order is total.

• decidableLE : DecidableRel fun (x x_1 : α) => x x_1

In a linearly ordered type, we assume the order relations are all decidable.

• decidableEq :

In a linearly ordered type, we assume the order relations are all decidable.

• decidableLT : DecidableRel fun (x x_1 : α) => x < x_1

In a linearly ordered type, we assume the order relations are all decidable.

• min_def : ∀ (a b : α), min a b = if a b then a else b

The minimum function is equivalent to the one you get from minOfLe.

• max_def : ∀ (a b : α), max a b = if a b then b else a

The minimum function is equivalent to the one you get from maxOfLe.

• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =

Comparison via compare is equal to the canonical comparison given decidable < and =.

Instances
class LinearOrderedCommGroup (α : Type u) extends , , , :

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 : α), = 1
• npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = * x
• inv : αα
• div : ααα
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹
• zpow : αα
• zpow_zero' : ∀ (a : α), = 1
• zpow_succ' : ∀ (n : ) (a : α), DivInvMonoid.zpow (Int.ofNat n.succ) a = * a
• zpow_neg' : ∀ (n : ) (a : α), = (DivInvMonoid.zpow (↑n.succ) a)⁻¹
• mul_left_inv : ∀ (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 bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = 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

A linear order is total.

• decidableLE : DecidableRel fun (x x_1 : α) => x x_1

In a linearly ordered type, we assume the order relations are all decidable.

• decidableEq :

In a linearly ordered type, we assume the order relations are all decidable.

• decidableLT : DecidableRel fun (x x_1 : α) => x < x_1

In a linearly ordered type, we assume the order relations are all decidable.

• min_def : ∀ (a b : α), min a b = if a b then a else b

The minimum function is equivalent to the one you get from minOfLe.

• max_def : ∀ (a b : α), max a b = if a b then b else a

The minimum function is equivalent to the one you get from maxOfLe.

• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =

Comparison via compare is equal to the canonical comparison given decidable < and =.

Instances
theorem LinearOrderedAddCommGroup.add_lt_add_left {α : Type u} (a : α) (b : α) (h : a < b) (c : α) :
c + a < c + b
theorem LinearOrderedCommGroup.mul_lt_mul_left' {α : Type u} (a : α) (b : α) (h : a < b) (c : α) :
c * a < c * b
theorem eq_zero_of_neg_eq {α : Type u} {a : α} (h : -a = a) :
a = 0
abbrev eq_zero_of_neg_eq.match_1 {α : Type u_1} {a : α} (motive : a < 0 a = 0 0 < aProp) :
∀ (x : a < 0 a = 0 0 < a), (∀ (h₁ : a < 0), motive )(∀ (h₁ : a = 0), motive )(∀ (h₁ : 0 < a), motive )motive x
Equations
• =
Instances For
theorem eq_one_of_inv_eq' {α : Type u} {a : α} (h : a⁻¹ = a) :
a = 1
theorem exists_zero_lt {α : Type u} [] :
∃ (a : α), 0 < a
theorem exists_one_lt' {α : Type u} [] :
∃ (a : α), 1 < a
@[instance 100]
Equations
• =
@[instance 100]
Equations
• =
@[instance 100]
Equations
• =
@[instance 100]
Equations
• =
theorem LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid.proof_2 {α : Type u_1} (a : α) (b : α) :
a b∀ (c : α), c + a c + b
@[instance 100]
Equations
• One or more equations did not get rendered due to their size.
@[instance 100]
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem neg_le_self_iff {α : Type u} {a : α} :
-a a 0 a
@[simp]
theorem inv_le_self_iff {α : Type u} {a : α} :
a⁻¹ a 1 a
@[simp]
theorem neg_lt_self_iff {α : Type u} {a : α} :
-a < a 0 < a
@[simp]
theorem inv_lt_self_iff {α : Type u} {a : α} :
a⁻¹ < a 1 < a
@[simp]
theorem le_neg_self_iff {α : Type u} {a : α} :
a -a a 0
@[simp]
theorem le_inv_self_iff {α : Type u} {a : α} :
a a⁻¹ a 1
@[simp]
theorem lt_neg_self_iff {α : Type u} {a : α} :
a < -a a < 0
@[simp]
theorem lt_inv_self_iff {α : Type u} {a : α} :
a < a⁻¹ a < 1
theorem neg_le_neg {α : Type u} {a : α} {b : α} :
a b-b -a
theorem inv_le_inv' {α : Type u} [] {a : α} {b : α} :
a bb⁻¹ a⁻¹
theorem neg_lt_neg {α : Type u} {a : α} {b : α} :
a < b-b < -a
theorem inv_lt_inv' {α : Type u} [] {a : α} {b : α} :
a < bb⁻¹ < a⁻¹
theorem neg_neg_of_pos {α : Type u} {a : α} :
0 < a-a < 0
theorem inv_lt_one_of_one_lt {α : Type u} [] {a : α} :
1 < aa⁻¹ < 1
theorem neg_nonpos_of_nonneg {α : Type u} {a : α} :
0 a-a 0
theorem inv_le_one_of_one_le {α : Type u} [] {a : α} :
1 aa⁻¹ 1
theorem neg_nonneg_of_nonpos {α : Type u} {a : α} :
a 00 -a
theorem one_le_inv_of_le_one {α : Type u} [] {a : α} :
a 11 a⁻¹