Documentation

Mathlib.Algebra.Order.Group.Defs

Ordered groups #

This file develops the basics of ordered groups.

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.

  • Addition is monotone in a ordered additive commutative group.

    add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b

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 :
    • Multiplication is monotone in a ordered commutative group.

      mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b

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

    Instances
      def OrderedAddCommGroup.to_covariantClass_left_le.proof_1 (α : Type u_1) [inst : OrderedAddCommGroup α] :
      CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1
      Equations
      def OrderedAddCommGroup.toOrderedCancelAddCommMonoid.proof_2 {α : Type u_1} [inst : OrderedAddCommGroup α] (a : α) (b : α) (c : α) (bc : a + b a + c) :
      b c
      Equations
      Equations
      • One or more equations did not get rendered due to their size.
      def OrderedAddCommGroup.toOrderedCancelAddCommMonoid.proof_1 {α : Type u_1} [inst : OrderedAddCommGroup α] (a : α) (b : α) :
      a + b = b + a
      Equations
      • (_ : ∀ (a b : α), a + b = b + a) = (_ : ∀ (a b : α), a + b = b + a)
      Equations
      def OrderedAddCommGroup.to_contravariantClass_left_le.proof_1 (α : Type u_1) [inst : OrderedAddCommGroup α] :
      ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1
      Equations
      def OrderedAddCommGroup.to_contravariantClass_right_le.proof_1 (α : Type u_1) [inst : OrderedAddCommGroup α] :
      ContravariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1
      Equations
      @[simp]
      theorem Left.neg_nonpos_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} :
      -a 0 0 a

      Uses left co(ntra)variant.

      @[simp]
      theorem Left.inv_le_one_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} :
      a⁻¹ 1 1 a

      Uses left co(ntra)variant.

      @[simp]
      theorem Left.nonneg_neg_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} :
      0 -a a 0

      Uses left co(ntra)variant.

      @[simp]
      theorem Left.one_le_inv_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} :
      1 a⁻¹ a 1

      Uses left co(ntra)variant.

      @[simp]
      theorem le_neg_add_iff_add_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      b -a + c a + b c
      @[simp]
      theorem le_inv_mul_iff_mul_le {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      b a⁻¹ * c a * b c
      @[simp]
      theorem neg_add_le_iff_le_add {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      -b + a c a b + c
      @[simp]
      theorem inv_mul_le_iff_le_mul {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      b⁻¹ * a c a b * c
      theorem neg_le_iff_add_nonneg' {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      -a b 0 a + b
      theorem inv_le_iff_one_le_mul' {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      a⁻¹ b 1 a * b
      theorem le_neg_iff_add_nonpos_left {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      a -b b + a 0
      theorem le_inv_iff_mul_le_one_left {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      a b⁻¹ b * a 1
      theorem le_neg_add_iff_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      0 -b + a b a
      theorem le_inv_mul_iff_le {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      1 b⁻¹ * a b a
      theorem neg_add_nonpos_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      -a + b 0 b a
      theorem inv_mul_le_one_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      a⁻¹ * b 1 b a
      @[simp]
      theorem Left.neg_pos_iff {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} :
      0 < -a a < 0

      Uses left co(ntra)variant.

      @[simp]
      theorem Left.one_lt_inv_iff {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} :
      1 < a⁻¹ a < 1

      Uses left co(ntra)variant.

      @[simp]
      theorem Left.neg_neg_iff {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} :
      -a < 0 0 < a

      Uses left co(ntra)variant.

      @[simp]
      theorem Left.inv_lt_one_iff {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} :
      a⁻¹ < 1 1 < a

      Uses left co(ntra)variant.

      @[simp]
      theorem lt_neg_add_iff_add_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      b < -a + c a + b < c
      @[simp]
      theorem lt_inv_mul_iff_mul_lt {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      b < a⁻¹ * c a * b < c
      @[simp]
      theorem neg_add_lt_iff_lt_add {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      -b + a < c a < b + c
      @[simp]
      theorem inv_mul_lt_iff_lt_mul {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      b⁻¹ * a < c a < b * c
      theorem neg_lt_iff_pos_add' {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      -a < b 0 < a + b
      theorem inv_lt_iff_one_lt_mul' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a⁻¹ < b 1 < a * b
      theorem lt_neg_iff_add_neg' {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a < -b b + a < 0
      theorem lt_inv_iff_mul_lt_one' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a < b⁻¹ b * a < 1
      theorem lt_neg_add_iff_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      0 < -b + a b < a
      theorem lt_inv_mul_iff_lt {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      1 < b⁻¹ * a b < a
      theorem neg_add_neg_iff {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      -a + b < 0 b < a
      theorem inv_mul_lt_one_iff {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a⁻¹ * b < 1 b < a
      @[simp]
      theorem Right.neg_nonpos_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} :
      -a 0 0 a

      Uses right co(ntra)variant.

      @[simp]
      theorem Right.inv_le_one_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} :
      a⁻¹ 1 1 a

      Uses right co(ntra)variant.

      @[simp]
      theorem Right.nonneg_neg_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} :
      0 -a a 0

      Uses right co(ntra)variant.

      @[simp]
      theorem Right.one_le_inv_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} :
      1 a⁻¹ a 1

      Uses right co(ntra)variant.

      theorem neg_le_iff_add_nonneg {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      -a b 0 b + a
      theorem inv_le_iff_one_le_mul {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      a⁻¹ b 1 b * a
      theorem le_neg_iff_add_nonpos_right {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      a -b a + b 0
      theorem le_inv_iff_mul_le_one_right {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      a b⁻¹ a * b 1
      @[simp]
      theorem add_neg_le_iff_le_add {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a + -b c a c + b
      @[simp]
      theorem mul_inv_le_iff_le_mul {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a * b⁻¹ c a c * b
      @[simp]
      theorem le_add_neg_iff_add_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      c a + -b c + b a
      @[simp]
      theorem le_mul_inv_iff_mul_le {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      c a * b⁻¹ c * b a
      theorem add_neg_nonpos_iff_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      a + -b 0 a b
      theorem mul_inv_le_one_iff_le {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      a * b⁻¹ 1 a b
      theorem le_add_neg_iff_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      0 a + -b b a
      theorem le_mul_inv_iff_le {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      1 a * b⁻¹ b a
      theorem add_neg_nonpos_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      b + -a 0 b a
      theorem mul_inv_le_one_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      b * a⁻¹ 1 b a
      @[simp]
      theorem Right.neg_neg_iff {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} :
      -a < 0 0 < a

      Uses right co(ntra)variant.

      @[simp]
      theorem Right.inv_lt_one_iff {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} :
      a⁻¹ < 1 1 < a

      Uses right co(ntra)variant.

      @[simp]
      theorem Right.neg_pos_iff {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} :
      0 < -a a < 0

      Uses right co(ntra)variant.

      @[simp]
      theorem Right.one_lt_inv_iff {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} :
      1 < a⁻¹ a < 1

      Uses right co(ntra)variant.

      theorem neg_lt_iff_pos_add {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      -a < b 0 < b + a
      theorem inv_lt_iff_one_lt_mul {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a⁻¹ < b 1 < b * a
      theorem lt_neg_iff_add_neg {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a < -b a + b < 0
      theorem lt_inv_iff_mul_lt_one {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a < b⁻¹ a * b < 1
      @[simp]
      theorem add_neg_lt_iff_lt_add {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a + -b < c a < c + b
      @[simp]
      theorem mul_inv_lt_iff_lt_mul {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a * b⁻¹ < c a < c * b
      @[simp]
      theorem lt_add_neg_iff_add_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      c < a + -b c + b < a
      @[simp]
      theorem lt_mul_inv_iff_mul_lt {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      c < a * b⁻¹ c * b < a
      theorem neg_add_neg_iff_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a + -b < 0 a < b
      theorem inv_mul_lt_one_iff_lt {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a * b⁻¹ < 1 a < b
      theorem lt_add_neg_iff_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      0 < a + -b b < a
      theorem lt_mul_inv_iff_lt {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      1 < a * b⁻¹ b < a
      theorem add_neg_neg_iff {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      b + -a < 0 b < a
      theorem mul_inv_lt_one_iff {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      b * a⁻¹ < 1 b < a
      @[simp]
      theorem neg_le_neg_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      -a -b b a
      @[simp]
      theorem inv_le_inv_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      theorem le_of_neg_le_neg {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      -a -bb a

      Alias of the forward direction of neg_le_neg_iff.

      theorem add_neg_le_neg_add_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} {d : α} :
      a + -b -d + c d + a c + b
      theorem mul_inv_le_inv_mul_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} {d : α} :
      a * b⁻¹ d⁻¹ * c d * a c * b
      @[simp]
      theorem sub_le_self_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] (a : α) {b : α} :
      a - b a 0 b
      @[simp]
      theorem div_le_self_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] (a : α) {b : α} :
      a / b a 1 b
      @[simp]
      theorem le_sub_self_iff {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] (a : α) {b : α} :
      a a - b b 0
      @[simp]
      theorem le_div_self_iff {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] (a : α) {b : α} :
      a a / b b 1
      theorem sub_le_self {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] (a : α) {b : α} :
      0 ba - b a

      Alias of the reverse direction of sub_le_self_iff.

      @[simp]
      theorem neg_lt_neg_iff {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      -a < -b b < a
      @[simp]
      theorem inv_lt_inv_iff {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a⁻¹ < b⁻¹ b < a
      theorem neg_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      -a < b -b < a
      theorem inv_lt' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a⁻¹ < b b⁻¹ < a
      theorem lt_neg {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a < -b b < -a
      theorem lt_inv' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a < b⁻¹ b < a⁻¹
      theorem lt_inv_of_lt_inv {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a < b⁻¹b < a⁻¹

      Alias of the forward direction of lt_inv'.

      theorem lt_neg_of_lt_neg {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a < -bb < -a
      theorem inv_lt_of_inv_lt' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a⁻¹ < bb⁻¹ < a

      Alias of the forward direction of inv_lt'.

      theorem neg_lt_of_neg_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      -a < b-b < a
      theorem add_neg_lt_neg_add_iff {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} :
      a + -b < -d + c d + a < c + b
      theorem mul_inv_lt_inv_mul_iff {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} :
      a * b⁻¹ < d⁻¹ * c d * a < c * b
      @[simp]
      theorem sub_lt_self_iff {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α} :
      a - b < a 0 < b
      @[simp]
      theorem div_lt_self_iff {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] (a : α) {b : α} :
      a / b < a 1 < b
      theorem sub_lt_self {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] (a : α) {b : α} :
      0 < ba - b < a

      Alias of the reverse direction of sub_lt_self_iff.

      theorem Left.neg_le_self {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} (h : 0 a) :
      -a a
      theorem Left.inv_le_self {α : Type u} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} (h : 1 a) :
      theorem neg_le_self {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} (h : 0 a) :
      -a a

      Alias of Left.neg_le_self.

      theorem Left.self_le_neg {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} (h : a 0) :
      a -a
      theorem Left.self_le_inv {α : Type u} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} (h : a 1) :
      theorem Left.neg_lt_self {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} (h : 0 < a) :
      -a < a
      theorem Left.inv_lt_self {α : Type u} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} (h : 1 < a) :
      a⁻¹ < a
      theorem neg_lt_self {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} (h : 0 < a) :
      -a < a

      Alias of Left.neg_lt_self.

      theorem Left.self_lt_neg {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} (h : a < 0) :
      a < -a
      theorem Left.self_lt_inv {α : Type u} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} (h : a < 1) :
      a < a⁻¹
      theorem Right.neg_le_self {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} (h : 0 a) :
      -a a
      theorem Right.inv_le_self {α : Type u} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} (h : 1 a) :
      theorem Right.self_le_neg {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} (h : a 0) :
      a -a
      theorem Right.self_le_inv {α : Type u} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} (h : a 1) :
      theorem Right.neg_lt_self {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} (h : 0 < a) :
      -a < a
      theorem Right.inv_lt_self {α : Type u} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} (h : 1 < a) :
      a⁻¹ < a
      theorem Right.self_lt_neg {α : Type u} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} (h : a < 0) :
      a < -a
      theorem Right.self_lt_inv {α : Type u} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} (h : a < 1) :
      a < a⁻¹
      theorem neg_add_le_iff_le_add' {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      -c + a b a b + c
      theorem inv_mul_le_iff_le_mul' {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      c⁻¹ * a b a b * c
      theorem add_neg_le_iff_le_add' {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a + -b c a b + c
      theorem mul_inv_le_iff_le_mul' {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a * b⁻¹ c a b * c
      theorem add_neg_le_add_neg_iff {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} {d : α} :
      a + -b c + -d a + d c + b
      theorem mul_inv_le_mul_inv_iff' {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} {d : α} :
      a * b⁻¹ c * d⁻¹ a * d c * b
      theorem neg_add_lt_iff_lt_add' {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      -c + a < b a < b + c
      theorem inv_mul_lt_iff_lt_mul' {α : Type u} [inst : CommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      c⁻¹ * a < b a < b * c
      theorem add_neg_lt_iff_le_add' {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a + -b < c a < b + c
      theorem mul_inv_lt_iff_le_mul' {α : Type u} [inst : CommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a * b⁻¹ < c a < b * c
      theorem add_neg_lt_add_neg_iff {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} :
      a + -b < c + -d a + d < c + b
      theorem mul_inv_lt_mul_inv_iff' {α : Type u} [inst : CommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} :
      a * b⁻¹ < c * d⁻¹ a * d < c * b
      theorem one_le_of_inv_le_one {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} :
      a⁻¹ 11 a

      Alias of the forward direction of Left.inv_le_one_iff.

      theorem nonneg_of_neg_nonpos {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} :
      -a 00 a
      theorem le_one_of_one_le_inv {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} :
      1 a⁻¹a 1

      Alias of the forward direction of Left.one_le_inv_iff.

      theorem nonpos_of_neg_nonneg {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} :
      0 -aa 0
      theorem lt_of_inv_lt_inv {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a⁻¹ < b⁻¹b < a

      Alias of the forward direction of inv_lt_inv_iff.

      theorem lt_of_neg_lt_neg {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      -a < -bb < a
      theorem one_lt_of_inv_lt_one {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} :
      a⁻¹ < 11 < a

      Alias of the forward direction of Left.inv_lt_one_iff.

      theorem pos_of_neg_neg {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} :
      -a < 00 < a
      theorem inv_lt_one_iff_one_lt {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} :
      a⁻¹ < 1 1 < a

      Alias of Left.inv_lt_one_iff.

      theorem neg_neg_iff_pos {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} :
      -a < 0 0 < a
      theorem inv_lt_one' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} :
      a⁻¹ < 1 1 < a

      Alias of Left.inv_lt_one_iff.

      theorem neg_lt_zero {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} :
      -a < 0 0 < a
      theorem inv_of_one_lt_inv {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} :
      1 < a⁻¹a < 1

      Alias of the forward direction of Left.one_lt_inv_iff.

      theorem neg_of_neg_pos {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} :
      0 < -aa < 0
      theorem one_lt_inv_of_inv {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} :
      a < 11 < a⁻¹

      Alias of the reverse direction of Left.one_lt_inv_iff.

      theorem neg_pos_of_neg {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} :
      a < 00 < -a
      theorem mul_le_of_le_inv_mul {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      b a⁻¹ * ca * b c

      Alias of the forward direction of le_inv_mul_iff_mul_le.

      theorem add_le_of_le_neg_add {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      b -a + ca + b c
      theorem le_inv_mul_of_mul_le {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a * b cb a⁻¹ * c

      Alias of the reverse direction of le_inv_mul_iff_mul_le.

      theorem le_neg_add_of_add_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a + b cb -a + c
      theorem inv_mul_le_of_le_mul {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a b * cb⁻¹ * a c

      Alias of the reverse direction of inv_mul_le_iff_le_mul.

      theorem neg_add_le_of_le_add {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a b + c-b + a c
      theorem mul_lt_of_lt_inv_mul {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      b < a⁻¹ * ca * b < c

      Alias of the forward direction of lt_inv_mul_iff_mul_lt.

      theorem add_lt_of_lt_neg_add {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      b < -a + ca + b < c
      theorem lt_inv_mul_of_mul_lt {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a * b < cb < a⁻¹ * c

      Alias of the reverse direction of lt_inv_mul_iff_mul_lt.

      theorem lt_neg_add_of_add_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a + b < cb < -a + c
      theorem lt_mul_of_inv_mul_lt {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      b⁻¹ * a < ca < b * c

      Alias of the forward direction of inv_mul_lt_iff_lt_mul.

      theorem inv_mul_lt_of_lt_mul {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a < b * cb⁻¹ * a < c

      Alias of the reverse direction of inv_mul_lt_iff_lt_mul.

      theorem lt_add_of_neg_add_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      -b + a < ca < b + c
      theorem neg_add_lt_of_lt_add {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a < b + c-b + a < c
      theorem lt_mul_of_inv_mul_lt_left {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      b⁻¹ * a < ca < b * c

      Alias of lt_mul_of_inv_mul_lt.

      theorem lt_add_of_neg_add_lt_left {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      -b + a < ca < b + c
      theorem inv_le_one' {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} :
      a⁻¹ 1 1 a

      Alias of Left.inv_le_one_iff.

      theorem neg_nonpos {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} :
      -a 0 0 a
      theorem one_le_inv' {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} :
      1 a⁻¹ a 1

      Alias of Left.one_le_inv_iff.

      theorem neg_nonneg {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} :
      0 -a a 0
      theorem one_lt_inv' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} :
      1 < a⁻¹ a < 1

      Alias of Left.one_lt_inv_iff.

      theorem neg_pos {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} :
      0 < -a a < 0
      theorem OrderedCommGroup.mul_lt_mul_left' {α : Type u_1} [inst : Mul α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {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} [inst : Add α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {b : α} {c : α} (bc : b < c) (a : α) :
      a + b < a + c
      theorem OrderedCommGroup.le_of_mul_le_mul_left {α : Type u_1} [inst : Mul α] [inst : LE α] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {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} [inst : Add α] [inst : LE α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} (bc : a + b a + c) :
      b c
      theorem OrderedCommGroup.lt_of_mul_lt_mul_left {α : Type u_1} [inst : Mul α] [inst : LT α] [inst : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {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} [inst : Add α] [inst : LT α] [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} (bc : a + b < a + c) :
      b < c
      @[simp]
      theorem sub_le_sub_iff_right {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} (c : α) :
      a - c b - c a b
      @[simp]
      theorem div_le_div_iff_right {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} (c : α) :
      a / c b / c a b
      theorem sub_le_sub_right {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} (h : a b) (c : α) :
      a - c b - c
      theorem div_le_div_right' {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} (h : a b) (c : α) :
      a / c b / c
      @[simp]
      theorem sub_nonneg {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      0 a - b b a
      @[simp]
      theorem one_le_div' {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      1 a / b b a
      theorem sub_nonneg_of_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      b a0 a - b

      Alias of the reverse direction of sub_nonneg.

      theorem le_of_sub_nonneg {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      0 a - bb a

      Alias of the forward direction of sub_nonneg.

      @[simp]
      theorem sub_nonpos {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      a - b 0 a b
      @[simp]
      theorem div_le_one' {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      a / b 1 a b
      theorem sub_nonpos_of_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      a ba - b 0

      Alias of the reverse direction of sub_nonpos.

      theorem le_of_sub_nonpos {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      a - b 0a b

      Alias of the forward direction of sub_nonpos.

      theorem le_sub_iff_add_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a c - b a + b c
      theorem le_div_iff_mul_le {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a c / b a * b c
      theorem le_sub_right_of_add_le {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a + b ca c - b

      Alias of the reverse direction of le_sub_iff_add_le.

      theorem add_le_of_le_sub_right {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a c - ba + b c

      Alias of the forward direction of le_sub_iff_add_le.

      theorem sub_le_iff_le_add {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a - c b a b + c
      theorem div_le_iff_le_mul {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a / c b a b * c
      instance AddGroup.toHasOrderedSub {α : Type u_1} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] :
      Equations
      • AddGroup.toHasOrderedSub = { tsub_le_iff_right := (_ : ∀ (x x_1 x_2 : α), x - x_1 x_2 x x_2 + x_1) }
      @[simp]
      theorem sub_le_sub_iff_left {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {b : α} {c : α} (a : α) :
      a - b a - c c b
      @[simp]
      theorem div_le_div_iff_left {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {b : α} {c : α} (a : α) :
      a / b a / c c b
      theorem sub_le_sub_left {α : Type u} [inst : AddGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} (h : a b) (c : α) :
      c - b c - a
      theorem div_le_div_left' {α : Type u} [inst : Group α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} (h : a b) (c : α) :
      c / b c / a
      theorem sub_le_sub_iff {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} {d : α} :
      a - b c - d a + d c + b
      theorem div_le_div_iff' {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} {d : α} :
      a / b c / d a * d c * b
      theorem le_sub_iff_add_le' {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      b c - a a + b c
      theorem le_div_iff_mul_le' {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      b c / a a * b c
      theorem add_le_of_le_sub_left {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      b c - aa + b c

      Alias of the forward direction of le_sub_iff_add_le'.

      theorem le_sub_left_of_add_le {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a + b cb c - a

      Alias of the reverse direction of le_sub_iff_add_le'.

      theorem sub_le_iff_le_add' {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a - b c a b + c
      theorem div_le_iff_le_mul' {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a / b c a b * c
      theorem sub_left_le_of_le_add {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a b + ca - b c

      Alias of the reverse direction of sub_le_iff_le_add'.

      theorem le_add_of_sub_left_le {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a - b ca b + c

      Alias of the forward direction of sub_le_iff_le_add'.

      @[simp]
      theorem neg_le_sub_iff_le_add {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      -b a - c c a + b
      @[simp]
      theorem inv_le_div_iff_le_mul {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      b⁻¹ a / c c a * b
      theorem neg_le_sub_iff_le_add' {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      -a b - c c a + b
      theorem inv_le_div_iff_le_mul' {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a⁻¹ b / c c a * b
      theorem sub_le_comm {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a - b c a - c b
      theorem div_le_comm {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a / b c a / c b
      theorem le_sub_comm {α : Type u} [inst : AddCommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a b - c c b - a
      theorem le_div_comm {α : Type u} [inst : CommGroup α] [inst : LE α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} :
      a b / c c b / a
      theorem sub_le_sub {α : Type u} [inst : AddCommGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} {d : α} (hab : a b) (hcd : c d) :
      a - d b - c
      theorem div_le_div'' {α : Type u} [inst : CommGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} {c : α} {d : α} (hab : a b) (hcd : c d) :
      a / d b / c
      @[simp]
      theorem sub_lt_sub_iff_right {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (c : α) :
      a - c < b - c a < b
      @[simp]
      theorem div_lt_div_iff_right {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (c : α) :
      a / c < b / c a < b
      theorem sub_lt_sub_right {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : a < b) (c : α) :
      a - c < b - c
      theorem div_lt_div_right' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : a < b) (c : α) :
      a / c < b / c
      @[simp]
      theorem sub_pos {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      0 < a - b b < a
      @[simp]
      theorem one_lt_div' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      1 < a / b b < a
      theorem sub_pos_of_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      b < a0 < a - b

      Alias of the reverse direction of sub_pos.

      theorem lt_of_sub_pos {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      0 < a - bb < a

      Alias of the forward direction of sub_pos.

      @[simp]
      theorem sub_neg {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a - b < 0 a < b
      @[simp]
      theorem div_lt_one' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a / b < 1 a < b
      theorem lt_of_sub_neg {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a - b < 0a < b

      Alias of the forward direction of sub_neg.

      theorem sub_neg_of_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a < ba - b < 0

      Alias of the reverse direction of sub_neg.

      theorem sub_lt_zero {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
      a - b < 0 a < b

      Alias of sub_neg.

      theorem lt_sub_iff_add_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a < c - b a + b < c
      theorem lt_div_iff_mul_lt {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a < c / b a * b < c
      theorem lt_sub_right_of_add_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a + b < ca < c - b

      Alias of the reverse direction of lt_sub_iff_add_lt.

      theorem add_lt_of_lt_sub_right {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a < c - ba + b < c

      Alias of the forward direction of lt_sub_iff_add_lt.

      theorem sub_lt_iff_lt_add {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a - c < b a < b + c
      theorem div_lt_iff_lt_mul {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a / c < b a < b * c
      theorem sub_right_lt_of_lt_add {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a < b + ca - c < b

      Alias of the reverse direction of sub_lt_iff_lt_add.

      theorem lt_add_of_sub_right_lt {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a - c < ba < b + c

      Alias of the forward direction of sub_lt_iff_lt_add.

      @[simp]
      theorem sub_lt_sub_iff_left {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {b : α} {c : α} (a : α) :
      a - b < a - c c < b
      @[simp]
      theorem div_lt_div_iff_left {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {b : α} {c : α} (a : α) :
      a / b < a / c c < b
      @[simp]
      theorem neg_lt_sub_iff_lt_add {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      -a < b - c c < a + b
      @[simp]
      theorem inv_lt_div_iff_lt_mul {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a⁻¹ < b / c c < a * b
      theorem sub_lt_sub_left {α : Type u} [inst : AddGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : a < b) (c : α) :
      c - b < c - a
      theorem div_lt_div_left' {α : Type u} [inst : Group α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : a < b) (c : α) :
      c / b < c / a
      theorem sub_lt_sub_iff {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} :
      a - b < c - d a + d < c + b
      theorem div_lt_div_iff' {α : Type u} [inst : CommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} :
      a / b < c / d a * d < c * b
      theorem lt_sub_iff_add_lt' {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      b < c - a a + b < c
      theorem lt_div_iff_mul_lt' {α : Type u} [inst : CommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      b < c / a a * b < c
      theorem lt_sub_left_of_add_lt {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a + b < cb < c - a

      Alias of the reverse direction of lt_sub_iff_add_lt'.

      theorem add_lt_of_lt_sub_left {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      b < c - aa + b < c

      Alias of the forward direction of lt_sub_iff_add_lt'.

      theorem sub_lt_iff_lt_add' {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a - b < c a < b + c
      theorem div_lt_iff_lt_mul' {α : Type u} [inst : CommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a / b < c a < b * c
      theorem lt_add_of_sub_left_lt {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a - b < ca < b + c

      Alias of the forward direction of sub_lt_iff_lt_add'.

      theorem sub_left_lt_of_lt_add {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a < b + ca - b < c

      Alias of the reverse direction of sub_lt_iff_lt_add'.

      theorem neg_lt_sub_iff_lt_add' {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      -b < a - c c < a + b
      theorem inv_lt_div_iff_lt_mul' {α : Type u} [inst : CommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      b⁻¹ < a / c c < a * b
      theorem sub_lt_comm {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a - b < c a - c < b
      theorem div_lt_comm {α : Type u} [inst : CommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a / b < c a / c < b
      theorem lt_sub_comm {α : Type u} [inst : AddCommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a < b - c c < b - a
      theorem lt_div_comm {α : Type u} [inst : CommGroup α] [inst : LT α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} :
      a < b / c c < b / a
      theorem sub_lt_sub {α : Type u} [inst : AddCommGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} (hab : a < b) (hcd : c < d) :
      a - d < b - c
      theorem div_lt_div'' {α : Type u} [inst : CommGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} {c : α} {d : α} (hab : a < b) (hcd : c < d) :
      a / d < b / c
      @[simp]
      theorem cmp_sub_zero {α : Type u} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] (a : α) (b : α) :
      cmp (a - b) 0 = cmp a b
      @[simp]
      theorem cmp_div_one' {α : Type u} [inst : Group α] [inst : LinearOrder α] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] (a : α) (b : α) :
      cmp (a / b) 1 = cmp a b
      theorem le_of_forall_pos_lt_add {α : Type u} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} (h : ∀ (ε : α), 0 < εa < b + ε) :
      a b
      theorem le_of_forall_one_lt_lt_mul {α : Type u} [inst : Group α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} (h : ∀ (ε : α), 1 < εa < b * ε) :
      a b
      theorem le_iff_forall_pos_lt_add {α : Type u} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      a b ∀ (ε : α), 0 < εa < b + ε
      theorem le_iff_forall_one_lt_lt_mul {α : Type u} [inst : Group α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      a b ∀ (ε : α), 1 < εa < b * ε
      theorem sub_le_neg_add_iff {α : Type u} [inst : AddGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] :
      a - b -a + b a b
      theorem div_le_inv_mul_iff {α : Type u} [inst : Group α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] :
      a / b a⁻¹ * b a b
      theorem sub_le_sub_flip {α : Type u_1} [inst : AddCommGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      a - b b - a a b
      @[simp]
      theorem div_le_div_flip {α : Type u_1} [inst : CommGroup α] [inst : LinearOrder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] {a : α} {b : α} :
      a / b b / a a b

      Linearly ordered commutative groups #

      • A linear order is total.

        le_total : ∀ (a b : α), a b b a
      • In a linearly ordered type, we assume the order relations are all decidable.

        decidable_le : DecidableRel fun x x_1 => x x_1
      • In a linearly ordered type, we assume the order relations are all decidable.

        decidable_eq : DecidableEq α
      • In a linearly ordered type, we assume the order relations are all decidable.

        decidable_lt : DecidableRel fun x x_1 => x < x_1
      • The minimum function is equivalent to the one you get from minOfLe.

        min_def : autoParam (∀ (a b : α), min a b = if a b then a else b) _auto✝
      • The minimum function is equivalent to the one you get from maxOfLe.

        max_def : autoParam (∀ (a b : α), max a b = if a b then b else a) _auto✝
      • Comparison via compare is equal to the canonical comparison given decidable < and =.

        compare_eq_compareOfLessAndEq : autoParam (∀ (a b : α), compare a b = compareOfLessAndEq a b) _auto✝

      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 monoid with an additively absorbing element. Instances should include number systems with an infinite element adjoined.`

        Instances
          class LinearOrderedCommGroup (α : Type u) extends OrderedCommGroup , Min , Max , Ord :
          • A linear order is total.

            le_total : ∀ (a b : α), a b b a
          • In a linearly ordered type, we assume the order relations are all decidable.

            decidable_le : DecidableRel fun x x_1 => x x_1
          • In a linearly ordered type, we assume the order relations are all decidable.

            decidable_eq : DecidableEq α
          • In a linearly ordered type, we assume the order relations are all decidable.

            decidable_lt : DecidableRel fun x x_1 => x < x_1
          • The minimum function is equivalent to the one you get from minOfLe.

            min_def : autoParam (∀ (a b : α), min a b = if a b then a else b) _auto✝
          • The minimum function is equivalent to the one you get from maxOfLe.

            max_def : autoParam (∀ (a b : α), max a b = if a b then b else a) _auto✝
          • Comparison via compare is equal to the canonical comparison given decidable < and =.

            compare_eq_compareOfLessAndEq : autoParam (∀ (a b : α), compare a b = compareOfLessAndEq a b) _auto✝

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

          Instances
            theorem LinearOrderedAddCommGroup.add_lt_add_left {α : Type u} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) (h : a < b) (c : α) :
            c + a < c + b
            theorem LinearOrderedCommGroup.mul_lt_mul_left' {α : Type u} [inst : LinearOrderedCommGroup α] (a : α) (b : α) (h : a < b) (c : α) :
            c * a < c * b
            abbrev eq_zero_of_neg_eq.match_1 {α : Type u_1} [inst : LinearOrderedAddCommGroup α] {a : α} (motive : a < 0 a = 0 0 < aProp) :
            (x : a < 0 a = 0 0 < a) → ((h₁ : a < 0) → motive (_ : a < 0 a = 0 0 < a)) → ((h₁ : a = 0) → motive (_ : a < 0 a = 0 0 < a)) → ((h₁ : 0 < a) → motive (_ : a < 0 a = 0 0 < a)) → motive x
            Equations
            theorem eq_zero_of_neg_eq {α : Type u} [inst : LinearOrderedAddCommGroup α] {a : α} (h : -a = a) :
            a = 0
            theorem eq_one_of_inv_eq' {α : Type u} [inst : LinearOrderedCommGroup α] {a : α} (h : a⁻¹ = a) :
            a = 1
            theorem exists_zero_lt {α : Type u} [inst : LinearOrderedAddCommGroup α] [inst : Nontrivial α] :
            a, 0 < a
            theorem exists_one_lt' {α : Type u} [inst : LinearOrderedCommGroup α] [inst : Nontrivial α] :
            a, 1 < a
            def LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid.proof_1 {α : Type u_1} [inst : LinearOrderedAddCommGroup α] (a : α) (b : α) :
            a b∀ (c : α), c + a c + b
            Equations
            • (_ : ∀ (a b : α), a b∀ (c : α), c + a c + b) = (_ : ∀ (a b : α), a b∀ (c : α), c + a c + b)
            Equations
            • One or more equations did not get rendered due to their size.
            Equations
            • One or more equations did not get rendered due to their size.
            structure AddCommGroup.PositiveCone (α : Type u_1) [inst : AddCommGroup α] :
            Type u_1
            • nonneg : αProp
            • pos : αProp
            • pos_iff : autoParam (∀ (a : α), pos a nonneg a ¬nonneg (-a)) _auto✝
            • zero_nonneg : nonneg 0
            • add_nonneg : {a b : α} → nonneg anonneg bnonneg (a + b)
            • nonneg_antisymm : ∀ {a : α}, nonneg anonneg (-a)a = 0

            A collection of elements in an AddCommGroup designated as "non-negative". This is useful for constructing an OrderedAddCommGroup by choosing a positive cone in an exisiting AddCommGroup.

            Instances For
              structure AddCommGroup.TotalPositiveCone (α : Type u_1) [inst : AddCommGroup α] extends AddCommGroup.PositiveCone :
              Type u_1

              A positive cone in an AddCommGroup induces a linear order if for every a, either a or -a is non-negative.

              Instances For

                Construct an OrderedAddCommGroup by designating a positive cone in an existing AddCommGroup.

                Equations

                Construct a LinearOrderedAddCommGroup by designating a positive cone in an existing AddCommGroup such that for every a, either a or -a is non-negative.

                Equations
                • One or more equations did not get rendered due to their size.
                theorem neg_le_neg {α : Type u} [inst : OrderedAddCommGroup α] {a : α} {b : α} :
                a b-b -a
                theorem inv_le_inv' {α : Type u} [inst : OrderedCommGroup α] {a : α} {b : α} :
                a bb⁻¹ a⁻¹
                theorem neg_lt_neg {α : Type u} [inst : OrderedAddCommGroup α] {a : α} {b : α} :
                a < b-b < -a
                theorem inv_lt_inv' {α : Type u} [inst : OrderedCommGroup α] {a : α} {b : α} :
                a < bb⁻¹ < a⁻¹
                theorem neg_neg_of_pos {α : Type u} [inst : OrderedAddCommGroup α] {a : α} :
                0 < a-a < 0
                theorem inv_lt_one_of_one_lt {α : Type u} [inst : OrderedCommGroup α] {a : α} :
                1 < aa⁻¹ < 1
                theorem neg_nonpos_of_nonneg {α : Type u} [inst : OrderedAddCommGroup α] {a : α} :
                0 a-a 0
                theorem inv_le_one_of_one_le {α : Type u} [inst : OrderedCommGroup α] {a : α} :
                1 aa⁻¹ 1
                theorem neg_nonneg_of_nonpos {α : Type u} [inst : OrderedAddCommGroup α] {a : α} :
                a 00 -a
                theorem one_le_inv_of_le_one {α : Type u} [inst : OrderedCommGroup α] {a : α} :
                a 11 a⁻¹
                theorem Monotone.neg {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : Preorder β] {f : βα} (hf : Monotone f) :
                Antitone fun x => -f x
                theorem Monotone.inv {α : Type u} {β : Type u_1} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : Preorder β] {f : βα} (hf : Monotone f) :
                Antitone fun x => (f x)⁻¹
                theorem Antitone.neg {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : Preorder β] {f : βα} (hf : Antitone f) :
                Monotone fun x => -f x
                theorem Antitone.inv {α : Type u} {β : Type u_1} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : Preorder β] {f : βα} (hf : Antitone f) :
                Monotone fun x => (f x)⁻¹
                theorem MonotoneOn.neg {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : Preorder β] {f : βα} {s : Set β} (hf : MonotoneOn f s) :
                AntitoneOn (fun x => -f x) s
                theorem MonotoneOn.inv {α : Type u} {β : Type u_1} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : Preorder β] {f : βα} {s : Set β} (hf : MonotoneOn f s) :
                AntitoneOn (fun x => (f x)⁻¹) s
                theorem AntitoneOn.neg {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] [inst : Preorder β] {f : βα} {s : Set β} (hf : AntitoneOn f s) :
                MonotoneOn (fun x => -f x) s
                theorem AntitoneOn.inv {α : Type u} {β : Type u_1} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1] [inst : Preorder β] {f : βα} {s : Set β} (hf : AntitoneOn f s) :
                MonotoneOn (fun x => (f x)⁻¹) s
                theorem StrictMono.neg {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : Preorder β] {f : βα} (hf : StrictMono f) :
                StrictAnti fun x => -f x
                theorem StrictMono.inv {α : Type u} {β : Type u_1} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : Preorder β] {f : βα} (hf : StrictMono f) :
                StrictAnti fun x => (f x)⁻¹
                theorem StrictAnti.neg {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : Preorder β] {f : βα} (hf : StrictAnti f) :
                StrictMono fun x => -f x
                theorem StrictAnti.inv {α : Type u} {β : Type u_1} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : Preorder β] {f : βα} (hf : StrictAnti f) :
                StrictMono fun x => (f x)⁻¹
                theorem StrictMonoOn.neg {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : Preorder β] {f : βα} {s : Set β} (hf : StrictMonoOn f s) :
                StrictAntiOn (fun x => -f x) s
                theorem StrictMonoOn.inv {α : Type u} {β : Type u_1} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : Preorder β] {f : βα} {s : Set β} (hf : StrictMonoOn f s) :
                StrictAntiOn (fun x => (f x)⁻¹) s
                theorem StrictAntiOn.neg {α : Type u} {β : Type u_1} [inst : AddGroup α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] [inst : Preorder β] {f : βα} {s : Set β} (hf : StrictAntiOn f s) :
                StrictMonoOn (fun x => -f x) s
                theorem StrictAntiOn.inv {α : Type u} {β : Type u_1} [inst : Group α] [inst : Preorder α] [inst : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x < x_1] [inst : Preorder β] {f : βα} {s : Set β} (hf : StrictAntiOn f s) :
                StrictMonoOn (fun x => (f x)⁻¹) s