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 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 (Int.ofNat n.succ) a = SubNegMonoid.zsmul (Int.ofNat 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.

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

Addition is monotone in an ordered additive commutative group.

class 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 (Int.ofNat n.succ) a = DivInvMonoid.zpow (Int.ofNat 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_le_mul_left {α : Type u} [self : OrderedCommGroup α] (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) [OrderedAddCommGroup α] : CovariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2

Equations

• ⋯ = ⋯

instance OrderedCommGroup.to_covariantClass_left_le (α : Type u) [OrderedCommGroup α] : CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2

Equations

• ⋯ = ⋯

theorem OrderedAddCommGroup.toOrderedCancelAddCommMonoid.proof_2 {α : Type u_1} [OrderedAddCommGroup α] (a : α) (b : α) (c : α) (bc : a + b ≤ a + c) : b ≤ c

theorem OrderedAddCommGroup.toOrderedCancelAddCommMonoid.proof_1 {α : Type u_1} [OrderedAddCommGroup α] (a : α) (b : α) : a + b = b + a

@[instance 100]

instance OrderedAddCommGroup.toOrderedCancelAddCommMonoid {α : Type u} [OrderedAddCommGroup α] : OrderedCancelAddCommMonoid α

Equations

• OrderedAddCommGroup.toOrderedCancelAddCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

@[instance 100]

instance OrderedCommGroup.toOrderedCancelCommMonoid {α : Type u} [OrderedCommGroup α] : OrderedCancelCommMonoid α

Equations

• OrderedCommGroup.toOrderedCancelCommMonoid = OrderedCancelCommMonoid.mk ⋯

theorem OrderedAddCommGroup.to_contravariantClass_left_le (α : Type u) [OrderedAddCommGroup α] : ContravariantClass α α (fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2

A choice-free shortcut instance.

theorem OrderedCommGroup.to_contravariantClass_left_le (α : Type u) [OrderedCommGroup α] : ContravariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2

A choice-free shortcut instance.

theorem OrderedAddCommGroup.to_contravariantClass_right_le (α : Type u) [OrderedAddCommGroup α] : ContravariantClass α α (Function.swap fun (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2

A choice-free shortcut instance.

theorem OrderedCommGroup.to_contravariantClass_right_le (α : Type u) [OrderedCommGroup α] : ContravariantClass α α (Function.swap fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2

A choice-free shortcut instance.

theorem OrderedCommGroup.mul_lt_mul_left' {α : Type u_1} [Mul α] [LT α] [CovariantClass α α (fun (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {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 (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {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 (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 ≤ x2] {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 (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 ≤ x2] {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 (x1 x2 : α) => x1 * x2) fun (x1 x2 : α) => x1 < x2] {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 (x1 x2 : α) => x1 + x2) fun (x1 x2 : α) => x1 < x2] {a : α} {b : α} {c : α} (bc : a + b < a + c) : b < c

Linearly ordered commutative groups

class LinearOrderedAddCommGroup (α : Type u) extends OrderedAddCommGroup , Min , Max , Ord : 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 (Int.ofNat n.succ) a = SubNegMonoid.zsmul (Int.ofNat 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

  A linear order is total.

• decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2

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

• decidableEq : DecidableEq α

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

• decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2

  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 = compareOfLessAndEq a b

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

class LinearOrderedCommGroup (α : Type u) extends OrderedCommGroup , Min , Max , Ord : 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 (Int.ofNat n.succ) a = DivInvMonoid.zpow (Int.ofNat 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

  A linear order is total.

• decidableLE : DecidableRel fun (x1 x2 : α) => x1 ≤ x2

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

• decidableEq : DecidableEq α

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

• decidableLT : DecidableRel fun (x1 x2 : α) => x1 < x2

  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 = compareOfLessAndEq a b

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

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

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

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

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

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

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

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

theorem LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid.proof_2 {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b

@[instance 100]

instance LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid {α : Type u} [LinearOrderedAddCommGroup α] : LinearOrderedCancelAddCommMonoid α

Equations

• One or more equations did not get rendered due to their size.

theorem LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid.proof_1 {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) : a + b = b + a

@[instance 100]

instance LinearOrderedCommGroup.toLinearOrderedCancelCommMonoid {α : Type u} [LinearOrderedCommGroup α] : LinearOrderedCancelCommMonoid α

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem neg_le_self_iff {α : Type u} [LinearOrderedAddCommGroup α] {a : α} : -a ≤ a ↔ 0 ≤ a

@[simp]

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

@[simp]

theorem neg_lt_self_iff {α : Type u} [LinearOrderedAddCommGroup α] {a : α} : -a < a ↔ 0 < a

@[simp]

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

@[simp]

theorem le_neg_self_iff {α : Type u} [LinearOrderedAddCommGroup α] {a : α} : a ≤ -a ↔ a ≤ 0

@[simp]

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

@[simp]

theorem lt_neg_self_iff {α : Type u} [LinearOrderedAddCommGroup α] {a : α} : a < -a ↔ a < 0

@[simp]

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

theorem neg_le_neg {α : Type u} [OrderedAddCommGroup α] {a : α} {b : α} : a ≤ b → -b ≤ -a

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

theorem neg_lt_neg {α : Type u} [OrderedAddCommGroup α] {a : α} {b : α} : a < b → -b < -a

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

theorem neg_neg_of_pos {α : Type u} [OrderedAddCommGroup α] {a : α} : 0 < a → -a < 0

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

theorem neg_nonpos_of_nonneg {α : Type u} [OrderedAddCommGroup α] {a : α} : 0 ≤ a → -a ≤ 0

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

theorem neg_nonneg_of_nonpos {α : Type u} [OrderedAddCommGroup α] {a : α} : a ≤ 0 → 0 ≤ -a

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