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.

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

Instances
class OrderedCommGroup (α : Type u) extends CommGroup α, PartialOrder α :

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

Instances

    A choice-free shortcut instance.

    A choice-free shortcut instance.

    A choice-free shortcut instance.

    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 #

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

    Instances

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

    Instances
      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]
      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 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 bb⁻¹ a⁻¹
      theorem neg_le_neg {α : Type u} [OrderedAddCommGroup α] {a b : α} :
      a b-b -a
      theorem inv_lt_inv' {α : Type u} [OrderedCommGroup α] {a b : α} :
      a < bb⁻¹ < 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 < aa⁻¹ < 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 aa⁻¹ 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 11 a⁻¹
      theorem neg_nonneg_of_nonpos {α : Type u} [OrderedAddCommGroup α] {a : α} :
      a 00 -a