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 , AddGroup , AddCommMonoid , SubNegMonoid , AddMonoid , Neg , Sub , AddCommSemigroup , AddSemigroup , AddZeroClass , Zero , AddCommMagma , Add , Preorder , LE , LT : Type u

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

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 , Group , CommMonoid , DivInvMonoid , Monoid , Inv , Div , CommSemigroup , Semigroup , MulOneClass , One , CommMagma , Mul , Preorder , LE , LT : Type u

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

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 OrderedCommGroup.toMulLeftMono (α : Type u) [OrderedCommGroup α] : MulLeftMono α

Equations

• ⋯ = ⋯

instance OrderedAddCommGroup.toAddLeftMono (α : Type u) [OrderedAddCommGroup α] : AddLeftMono α

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• OrderedCommGroup.toOrderedCancelCommMonoid = OrderedCancelCommMonoid.mk ⋯

@[instance 100]

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

Equations

• OrderedAddCommGroup.toOrderedCancelAddCommMonoid = OrderedCancelAddCommMonoid.mk ⋯

theorem OrderedCommGroup.toMulLeftReflectLE (α : Type u) [OrderedCommGroup α] : MulLeftReflectLE α

A choice-free shortcut instance.

theorem OrderedAddCommGroup.toAddLeftReflectLE (α : Type u) [OrderedAddCommGroup α] : AddLeftReflectLE α

A choice-free shortcut instance.

theorem OrderedCommGroup.toMulRightReflectLE (α : Type u) [OrderedCommGroup α] : MulRightReflectLE α

A choice-free shortcut instance.

theorem OrderedAddCommGroup.toAddRightReflectLE (α : Type u) [OrderedAddCommGroup α] : AddRightReflectLE α

A choice-free shortcut instance.

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

class LinearOrderedAddCommGroup (α : Type u) extends OrderedAddCommGroup , LinearOrder , AddCommGroup , PartialOrder , AddGroup , AddCommMonoid , SubNegMonoid , AddMonoid , Neg , Sub , AddCommSemigroup , AddSemigroup , AddZeroClass , Zero , AddCommMagma , Add , Min , Max , Ord , Preorder , LE , LT : Type u

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

class LinearOrderedCommGroup (α : Type u) extends OrderedCommGroup , LinearOrder , CommGroup , PartialOrder , Group , CommMonoid , DivInvMonoid , Monoid , Inv , Div , CommSemigroup , Semigroup , MulOneClass , One , CommMagma , Mul , Min , Max , Ord , Preorder , LE , LT : Type u

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} [LinearOrderedCommGroup α] (a : α) (b : α) (h : a < b) (c : α) : c * a < c * b

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

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

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

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

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

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

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

@[instance 100]

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

Equations

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

@[simp]

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

@[simp]

theorem neg_le_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 neg_lt_self_iff {α : Type u} [LinearOrderedAddCommGroup α] {a : α} : -a < a ↔ 0 < a

@[simp]

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

@[simp]

theorem le_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

@[simp]

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

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

theorem neg_le_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_lt_neg {α : Type u} [OrderedAddCommGroup α] {a : α} {b : α} : a < b → -b < -a

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

theorem neg_neg_of_pos {α : 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_nonpos_of_nonneg {α : Type u} [OrderedAddCommGroup α] {a : α} : 0 ≤ a → -a ≤ 0

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

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