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.

source
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'.

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

Alias of le_of_add_le_add_left.

source
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'.

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

Alias of lt_of_add_lt_add_left.

source
@[instance 100]
instance IsOrderedMonoid.toIsOrderedCancelMonoid {α : Type u} [CommGroup α] [Preorder α] [IsOrderedMonoid α] :
IsOrderedCancelMonoid α
source
@[instance 100]
instance IsOrderedAddMonoid.toIsOrderedCancelAddMonoid {α : Type u} [AddCommGroup α] [Preorder α] [IsOrderedAddMonoid α] :
IsOrderedCancelAddMonoid α
source
theorem IsOrderedMonoid.toIsOrderedCancelMonoid' {α : Type u} [CancelCommMonoid α] [LinearOrder α] [IsOrderedMonoid α] :
IsOrderedCancelMonoid α

Assuming α equipped with LinearOrder is CancelCommMonoid and IsOrderedMonoid, it is also IsOrderedCancelMonoid.

TODO: make it an instance. To avoid slowdown, it was not an instance when it was submitted. See https://github.com/leanprover-community/mathlib4/pull/32828.

source
theorem IsOrderedAddMonoid.toIsOrderedCancelAddMonoid' {α : Type u} [AddCancelCommMonoid α] [LinearOrder α] [IsOrderedAddMonoid α] :
IsOrderedCancelAddMonoid α

Assuming α equipped with LinearOrder is AddCancelCommMonoid and IsAddOrderedMonoid, it is also IsAddOrderedCancelMonoid.

TODO: make it an instance. To avoid slowdown, it was not an instance when it was submitted. See https://github.com/leanprover-community/mathlib4/pull/32828.

Linearly ordered commutative groups #

source
theorem eq_one_of_inv_eq' {α : Type u} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] {a : α} (h : a⁻¹ = a) :
a = 1
source
theorem eq_zero_of_neg_eq {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} (h : -a = a) :
a = 0
source
theorem exists_one_lt' {α : Type u} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [Nontrivial α] :
∃ (a : α), 1 < a
source
theorem exists_zero_lt {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Nontrivial α] :
∃ (a : α), 0 < a
source
@[instance 100]
instance LinearOrderedCommGroup.to_noMaxOrder {α : Type u} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [Nontrivial α] :
NoMaxOrder α
source
@[instance 100]
instance LinearOrderedAddCommGroup.to_noMaxOrder {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Nontrivial α] :
NoMaxOrder α
source
@[instance 100]
instance LinearOrderedCommGroup.to_noMinOrder {α : Type u} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] [Nontrivial α] :
NoMinOrder α
source
@[instance 100]
instance LinearOrderedAddCommGroup.to_noMinOrder {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [Nontrivial α] :
NoMinOrder α
source
@[simp]
theorem inv_le_self_iff {α : Type u} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] {a : α} :
a⁻¹ ≤ a ↔ 1 ≤ a
source
@[simp]
theorem neg_le_self_iff {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} :
-a ≤ a ↔ 0 ≤ a
source
@[simp]
theorem inv_lt_self_iff {α : Type u} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] {a : α} :
a⁻¹ < a ↔ 1 < a
source
@[simp]
theorem neg_lt_self_iff {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} :
-a < a ↔ 0 < a
source
@[simp]
theorem le_inv_self_iff {α : Type u} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] {a : α} :
a ≤ a⁻¹ ↔ a ≤ 1
source
@[simp]
theorem le_neg_self_iff {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} :
a ≤ -a ↔ a ≤ 0
source
@[simp]
theorem lt_inv_self_iff {α : Type u} [CommGroup α] [LinearOrder α] [IsOrderedMonoid α] {a : α} :
a < a⁻¹ ↔ a < 1
source
@[simp]
theorem lt_neg_self_iff {α : Type u} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {a : α} :
a < -a ↔ a < 0
source
theorem inv_le_inv' {α : Type u} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {a b : α} :
a ≤ b → b⁻¹ ≤ a⁻¹
source
theorem neg_le_neg {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b : α} :
a ≤ b → -b ≤ -a
source
theorem inv_lt_inv' {α : Type u} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {a b : α} :
a < b → b⁻¹ < a⁻¹
source
theorem neg_lt_neg {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a b : α} :
a < b → -b < -a
source
theorem inv_lt_one_of_one_lt {α : Type u} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {a : α} :
1 < a → a⁻¹ < 1
source
theorem neg_neg_of_pos {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a : α} :
0 < a → -a < 0
source
theorem inv_le_one_of_one_le {α : Type u} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {a : α} :
1 ≤ a → a⁻¹ ≤ 1
source
theorem neg_nonpos_of_nonneg {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a : α} :
0 ≤ a → -a ≤ 0
source
theorem one_le_inv_of_le_one {α : Type u} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {a : α} :
a ≤ 1 → 1 ≤ a⁻¹
source
theorem neg_nonneg_of_nonpos {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {a : α} :
a ≤ 0 → 0 ≤ -a