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

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

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

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

      source
      instance OrderedCommGroup.toMulLeftMono (α : Type u) [OrderedCommGroup α] :
      MulLeftMono α
      Equations
      • ⋯ = ⋯
      source
      instance OrderedAddCommGroup.toAddLeftMono (α : Type u) [OrderedAddCommGroup α] :
      AddLeftMono α
      Equations
      • ⋯ = ⋯
      source
      @[instance 100]
      instance OrderedCommGroup.toOrderedCancelCommMonoid {α : Type u} [OrderedCommGroup α] :
      OrderedCancelCommMonoid α
      Equations
      source
      @[instance 100]
      instance OrderedAddCommGroup.toOrderedCancelAddCommMonoid {α : Type u} [OrderedAddCommGroup α] :
      OrderedCancelAddCommMonoid α
      Equations
      source
      theorem OrderedCommGroup.toMulLeftReflectLE (α : Type u) [OrderedCommGroup α] :
      MulLeftReflectLE α

      A choice-free shortcut instance.

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

      A choice-free shortcut instance.

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

      A choice-free shortcut instance.

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

      A choice-free shortcut instance.

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

      source
      theorem OrderedAddCommGroup.add_lt_add_left {α : Type u_1} [Add α] [LT α] [AddLeftStrictMono α] {b : α} {c : α} (bc : b < c) (a : α) :
      a + b < a + c
      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 OrderedAddCommGroup.le_of_add_le_add_left {α : Type u_1} [Add α] [LE α] [AddLeftReflectLE α] {a : α} {b : α} {c : α} (bc : a + b ≤ a + c) :
      b ≤ c
      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 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 #

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

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

          Instances
          source
          theorem LinearOrderedCommGroup.mul_lt_mul_left' {α : Type u} [LinearOrderedCommGroup α] (a : α) (b : α) (h : a < b) (c : α) :
          c * a < c * b
          source
          theorem LinearOrderedAddCommGroup.add_lt_add_left {α : Type u} [LinearOrderedAddCommGroup α] (a : α) (b : α) (h : a < b) (c : α) :
          c + a < c + b
          source
          theorem eq_one_of_inv_eq' {α : Type u} [LinearOrderedCommGroup α] {a : α} (h : a⁻¹ = a) :
          a = 1
          source
          theorem eq_zero_of_neg_eq {α : Type u} [LinearOrderedAddCommGroup α] {a : α} (h : -a = a) :
          a = 0
          source
          theorem exists_one_lt' {α : Type u} [LinearOrderedCommGroup α] [Nontrivial α] :
          ∃ (a : α), 1 < a
          source
          theorem exists_zero_lt {α : Type u} [LinearOrderedAddCommGroup α] [Nontrivial α] :
          ∃ (a : α), 0 < a
          source
          @[instance 100]
          instance LinearOrderedCommGroup.to_noMaxOrder {α : Type u} [LinearOrderedCommGroup α] [Nontrivial α] :
          NoMaxOrder α
          Equations
          • ⋯ = ⋯
          source
          @[instance 100]
          instance LinearOrderedAddCommGroup.to_noMaxOrder {α : Type u} [LinearOrderedAddCommGroup α] [Nontrivial α] :
          NoMaxOrder α
          Equations
          • ⋯ = ⋯
          source
          @[instance 100]
          instance LinearOrderedCommGroup.to_noMinOrder {α : Type u} [LinearOrderedCommGroup α] [Nontrivial α] :
          NoMinOrder α
          Equations
          • ⋯ = ⋯
          source
          @[instance 100]
          instance LinearOrderedAddCommGroup.to_noMinOrder {α : Type u} [LinearOrderedAddCommGroup α] [Nontrivial α] :
          NoMinOrder α
          Equations
          • ⋯ = ⋯
          source
          @[instance 100]
          instance LinearOrderedCommGroup.toLinearOrderedCancelCommMonoid {α : Type u} [LinearOrderedCommGroup α] :
          LinearOrderedCancelCommMonoid α
          Equations
          • One or more equations did not get rendered due to their size.
          source
          @[instance 100]
          instance LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid {α : Type u} [LinearOrderedAddCommGroup α] :
          LinearOrderedCancelAddCommMonoid α
          Equations
          • One or more equations did not get rendered due to their size.
          source
          @[simp]
          theorem inv_le_self_iff {α : Type u} [LinearOrderedCommGroup α] {a : α} :
          a⁻¹ ≤ a ↔ 1 ≤ a
          source
          @[simp]
          theorem neg_le_self_iff {α : Type u} [LinearOrderedAddCommGroup α] {a : α} :
          -a ≤ a ↔ 0 ≤ a
          source
          @[simp]
          theorem inv_lt_self_iff {α : Type u} [LinearOrderedCommGroup α] {a : α} :
          a⁻¹ < a ↔ 1 < a
          source
          @[simp]
          theorem neg_lt_self_iff {α : Type u} [LinearOrderedAddCommGroup α] {a : α} :
          -a < a ↔ 0 < a
          source
          @[simp]
          theorem le_inv_self_iff {α : Type u} [LinearOrderedCommGroup α] {a : α} :
          a ≤ a⁻¹ ↔ a ≤ 1
          source
          @[simp]
          theorem le_neg_self_iff {α : Type u} [LinearOrderedAddCommGroup α] {a : α} :
          a ≤ -a ↔ a ≤ 0
          source
          @[simp]
          theorem lt_inv_self_iff {α : Type u} [LinearOrderedCommGroup α] {a : α} :
          a < a⁻¹ ↔ a < 1
          source
          @[simp]
          theorem lt_neg_self_iff {α : Type u} [LinearOrderedAddCommGroup α] {a : α} :
          a < -a ↔ a < 0
          source
          theorem inv_le_inv' {α : Type u} [OrderedCommGroup α] {a : α} {b : α} :
          a ≤ b → b⁻¹ ≤ a⁻¹
          source
          theorem neg_le_neg {α : Type u} [OrderedAddCommGroup α] {a : α} {b : α} :
          a ≤ b → -b ≤ -a
          source
          theorem inv_lt_inv' {α : Type u} [OrderedCommGroup α] {a : α} {b : α} :
          a < b → b⁻¹ < a⁻¹
          source
          theorem neg_lt_neg {α : Type u} [OrderedAddCommGroup α] {a : α} {b : α} :
          a < b → -b < -a
          source
          theorem inv_lt_one_of_one_lt {α : Type u} [OrderedCommGroup α] {a : α} :
          1 < a → a⁻¹ < 1
          source
          theorem neg_neg_of_pos {α : Type u} [OrderedAddCommGroup α] {a : α} :
          0 < a → -a < 0
          source
          theorem inv_le_one_of_one_le {α : Type u} [OrderedCommGroup α] {a : α} :
          1 ≤ a → a⁻¹ ≤ 1
          source
          theorem neg_nonpos_of_nonneg {α : Type u} [OrderedAddCommGroup α] {a : α} :
          0 ≤ a → -a ≤ 0
          source
          theorem one_le_inv_of_le_one {α : Type u} [OrderedCommGroup α] {a : α} :
          a ≤ 1 → 1 ≤ a⁻¹
          source
          theorem neg_nonneg_of_nonpos {α : Type u} [OrderedAddCommGroup α] {a : α} :
          a ≤ 0 → 0 ≤ -a