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.

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

Instances
    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 :

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

    Instances
      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
      @[instance 100]
      Equations
      @[instance 100]
      Equations
      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 #

      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 bb ca c
      • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
      • le_antisymm : ∀ (a b : α), a bb aa = 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 =.

      Instances
        class LinearOrderedCommGroup (α : Type u) extends OrderedCommGroup , Min , Max , Ord :

        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 bb ca c
        • lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
        • le_antisymm : ∀ (a b : α), a bb aa = 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 =.

        Instances
          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]
          Equations
          • =
          @[instance 100]
          Equations
          • =
          @[instance 100]
          Equations
          • =
          @[instance 100]
          Equations
          • =
          theorem LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid.proof_2 {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) :
          a b∀ (c : α), c + a c + b
          @[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 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 bb⁻¹ a⁻¹
          theorem neg_lt_neg {α : Type u} [OrderedAddCommGroup α] {a : α} {b : α} :
          a < b-b < -a
          theorem inv_lt_inv' {α : Type u} [OrderedCommGroup α] {a : α} {b : α} :
          a < bb⁻¹ < 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 < aa⁻¹ < 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 aa⁻¹ 1
          theorem neg_nonneg_of_nonpos {α : Type u} [OrderedAddCommGroup α] {a : α} :
          a 00 -a
          theorem one_le_inv_of_le_one {α : Type u} [OrderedCommGroup α] {a : α} :
          a 11 a⁻¹