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.

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 (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1
      Equations
      • =
      instance OrderedCommGroup.to_covariantClass_left_le (α : Type u) [OrderedCommGroup α] :
      CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1
      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 (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1

      A choice-free shortcut instance.

      theorem OrderedCommGroup.to_contravariantClass_left_le (α : Type u) [OrderedCommGroup α] :
      ContravariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1

      A choice-free shortcut instance.

      theorem OrderedAddCommGroup.to_contravariantClass_right_le (α : Type u) [OrderedAddCommGroup α] :
      ContravariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1

      A choice-free shortcut instance.

      theorem OrderedCommGroup.to_contravariantClass_right_le (α : Type u) [OrderedCommGroup α] :
      ContravariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1

      A choice-free shortcut instance.

      @[simp]
      theorem Left.neg_nonpos_iff {α : Type u} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [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} [Group α] [LE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [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} [AddGroup α] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [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} [AddGroup α] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [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} [Group α] [LE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [AddGroup α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [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} [Group α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [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} [AddGroup α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [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} [Group α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [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} [AddGroup α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [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} [Group α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [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} [Group α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [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} [AddGroup α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [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} [Group α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [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} [AddGroup α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [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} [AddGroup α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [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} [Group α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [AddGroup α] [Preorder α] [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} [Group α] [Preorder α] [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} [AddGroup α] [Preorder α] [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} [AddGroup α] [Preorder α] [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} [Group α] [Preorder α] [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} [AddGroup α] [Preorder α] [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} [Group α] [Preorder α] [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} [AddGroup α] [Preorder α] [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} [AddGroup α] [Preorder α] [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} [Group α] [Preorder α] [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} [AddGroup α] [Preorder α] [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} [Group α] [Preorder α] [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} [AddGroup α] [Preorder α] [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} [Group α] [Preorder α] [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} [AddGroup α] [Preorder α] [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} [Group α] [Preorder α] [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} [AddGroup α] [Preorder α] [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} [Group α] [Preorder α] [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} [AddCommGroup α] [LE α] [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} [CommGroup α] [LE α] [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} [AddCommGroup α] [LE α] [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} [CommGroup α] [LE α] [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} [AddCommGroup α] [LE α] [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} [CommGroup α] [LE α] [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} [AddCommGroup α] [LT α] [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} [CommGroup α] [LT α] [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} [AddCommGroup α] [LT α] [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} [CommGroup α] [LT α] [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} [AddCommGroup α] [LT α] [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} [CommGroup α] [LT α] [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} [Group α] [LE α] [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.


      Uses left co(ntra)variant.

      theorem nonneg_of_neg_nonpos {α : Type u} [AddGroup α] [LE α] [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} [Group α] [LE α] [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.


      Uses left co(ntra)variant.

      theorem nonpos_of_neg_nonneg {α : Type u} [AddGroup α] [LE α] [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} [Group α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [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} [AddGroup α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [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} [Group α] [LT α] [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.


      Uses left co(ntra)variant.

      theorem pos_of_neg_neg {α : Type u} [AddGroup α] [LT α] [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} [Group α] [LT α] [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.


      Uses left co(ntra)variant.

      theorem neg_neg_iff_pos {α : Type u} [AddGroup α] [LT α] [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} [Group α] [LT α] [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.


      Uses left co(ntra)variant.

      theorem neg_lt_zero {α : Type u} [AddGroup α] [LT α] [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} [Group α] [LT α] [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.


      Uses left co(ntra)variant.

      theorem neg_of_neg_pos {α : Type u} [AddGroup α] [LT α] [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} [Group α] [LT α] [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.


      Uses left co(ntra)variant.

      theorem neg_pos_of_neg {α : Type u} [AddGroup α] [LT α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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.


      Alias of the forward direction of inv_mul_lt_iff_lt_mul.

      theorem lt_add_of_neg_add_lt_left {α : Type u} [AddGroup α] [LT α] [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} [Group α] [LE α] [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.


      Uses left co(ntra)variant.

      theorem neg_nonpos {α : Type u} [AddGroup α] [LE α] [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} [Group α] [LE α] [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.


      Uses left co(ntra)variant.

      theorem neg_nonneg {α : Type u} [AddGroup α] [LE α] [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} [Group α] [LT α] [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.


      Uses left co(ntra)variant.

      theorem neg_pos {α : Type u} [AddGroup α] [LT α] [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} [Mul α] [LT α] [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} [Add α] [LT α] [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} [Mul α] [LE α] [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} [Add α] [LE α] [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} [Mul α] [LT α] [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} [Add α] [LT α] [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 sub_le_sub_iff_right {α : Type u} [AddGroup α] [LE α] [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 div_le_div_iff_right {α : Type u} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [AddGroup α] [LE α] [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.

      theorem sub_nonpos {α : Type u} [AddGroup α] [LE α] [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 div_le_one' {α : Type u} [Group α] [LE α] [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} [AddGroup α] [LE α] [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} [AddGroup α] [LE α] [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} [AddGroup α] [LE α] [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} [Group α] [LE α] [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 add_le_of_le_sub_right {α : Type u} [AddGroup α] [LE α] [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 le_sub_right_of_add_le {α : Type u} [AddGroup α] [LE α] [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 sub_le_iff_le_add {α : Type u} [AddGroup α] [LE α] [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
      @[simp]
      theorem div_le_iff_le_mul {α : Type u} [Group α] [LE α] [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 100]
      instance AddGroup.toOrderedSub {α : Type u_1} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] :
      Equations
      • =
      theorem sub_le_sub_iff_left {α : Type u} [AddGroup α] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [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 div_le_div_iff_left {α : Type u} [Group α] [LE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [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} [AddGroup α] [LE α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [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} [Group α] [LE α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [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} [AddCommGroup α] [LE α] [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} [CommGroup α] [LE α] [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} [AddCommGroup α] [LE α] [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} [CommGroup α] [LE α] [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_sub_left_of_add_le {α : Type u} [AddCommGroup α] [LE α] [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 add_le_of_le_sub_left {α : Type u} [AddCommGroup α] [LE α] [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 sub_le_iff_le_add' {α : Type u} [AddCommGroup α] [LE α] [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} [CommGroup α] [LE α] [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} [AddCommGroup α] [LE α] [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} [AddCommGroup α] [LE α] [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} [AddCommGroup α] [LE α] [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} [CommGroup α] [LE α] [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} [AddCommGroup α] [LE α] [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} [CommGroup α] [LE α] [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} [AddCommGroup α] [LE α] [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} [CommGroup α] [LE α] [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} [AddCommGroup α] [LE α] [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} [CommGroup α] [LE α] [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} [AddCommGroup α] [Preorder α] [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} [CommGroup α] [Preorder α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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} [AddGroup α] [LT α] [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} [Group α] [LT α] [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 lt_of_sub_pos {α : Type u} [AddGroup α] [LT α] [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.

      theorem sub_pos_of_lt {α : Type u} [AddGroup α] [LT α] [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.

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

      For a - -b = a + b, see sub_neg_eq_add.

      @[simp]
      theorem div_lt_one' {α : Type u} [Group α] [LT α] [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} [AddGroup α] [LT α] [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.


      For a - -b = a + b, see sub_neg_eq_add.

      theorem sub_neg_of_lt {α : Type u} [AddGroup α] [LT α] [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.


      For a - -b = a + b, see sub_neg_eq_add.

      theorem sub_lt_zero {α : Type u} [AddGroup α] [LT α] [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.


      For a - -b = a + b, see sub_neg_eq_add.

      theorem lt_sub_iff_add_lt {α : Type u} [AddGroup α] [LT α] [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} [Group α] [LT α] [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 add_lt_of_lt_sub_right {α : Type u} [AddGroup α] [LT α] [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 lt_sub_right_of_add_lt {α : Type u} [AddGroup α] [LT α] [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 sub_lt_iff_lt_add {α : Type u} [AddGroup α] [LT α] [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} [Group α] [LT α] [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_add_of_sub_right_lt {α : Type u} [AddGroup α] [LT α] [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.

      theorem sub_right_lt_of_lt_add {α : Type u} [AddGroup α] [LT α] [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.

      @[simp]
      theorem sub_lt_sub_iff_left {α : Type u} [AddGroup α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [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} [Group α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [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} [AddGroup α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [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} [Group α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [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} [AddGroup α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [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} [Group α] [LT α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [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} [AddCommGroup α] [LT α] [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} [CommGroup α] [LT α] [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} [AddCommGroup α] [LT α] [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} [CommGroup α] [LT α] [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} [AddCommGroup α] [LT α] [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} [AddCommGroup α] [LT α] [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} [AddCommGroup α] [LT α] [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} [CommGroup α] [LT α] [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} [AddCommGroup α] [LT α] [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} [AddCommGroup α] [LT α] [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} [AddCommGroup α] [LT α] [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} [CommGroup α] [LT α] [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} [AddCommGroup α] [LT α] [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} [CommGroup α] [LT α] [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} [AddCommGroup α] [LT α] [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} [CommGroup α] [LT α] [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} [AddCommGroup α] [Preorder α] [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} [CommGroup α] [Preorder α] [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 lt_or_lt_of_sub_lt_sub {α : Type u} [AddCommGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {a : α} {b : α} {c : α} {d : α} :
      a - d < b - ca < b c < d
      theorem lt_or_lt_of_div_lt_div {α : Type u} [CommGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {a : α} {b : α} {c : α} {d : α} :
      a / d < b / ca < b c < d
      @[simp]
      theorem cmp_sub_zero {α : Type u} [AddGroup α] [LinearOrder α] [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} [Group α] [LinearOrder α] [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} [AddGroup α] [LinearOrder α] [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} [Group α] [LinearOrder α] [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} [AddGroup α] [LinearOrder α] [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} [Group α] [LinearOrder α] [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} [AddGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {a : α} {b : α} [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} [Group α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] {a : α} {b : α} [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} [AddCommGroup α] [LinearOrder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] {a : α} {b : α} :
      a - b b - a a b
      theorem div_le_div_flip {α : Type u_1} [CommGroup α] [LinearOrder α] [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 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
      • add_left_neg : ∀ (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 (x x_1 : α) => x x_1

        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 (x x_1 : α) => x < x_1

        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

        A linearly ordered commutative group 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 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)⁻¹
          • mul_left_inv : ∀ (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 (x x_1 : α) => x x_1

            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 (x x_1 : α) => x < x_1

            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
            abbrev eq_zero_of_neg_eq.match_1 {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} (motive : a < 0 a = 0 0 < aProp) :
            ∀ (x : a < 0 a = 0 0 < a), (∀ (h₁ : a < 0), motive )(∀ (h₁ : a = 0), motive )(∀ (h₁ : 0 < a), motive )motive x
            Equations
            • =
            Instances For
              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
              • =
              @[instance 100]
              Equations
              • One or more equations did not get rendered due to their size.
              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.
              @[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⁻¹
              theorem Monotone.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Preorder β] {f : βα} (hf : Monotone f) :
              Antitone fun (x : β) => -f x
              theorem Monotone.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [Preorder β] {f : βα} (hf : Monotone f) :
              Antitone fun (x : β) => (f x)⁻¹
              theorem Antitone.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Preorder β] {f : βα} (hf : Antitone f) :
              Monotone fun (x : β) => -f x
              theorem Antitone.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [Preorder β] {f : βα} (hf : Antitone f) :
              Monotone fun (x : β) => (f x)⁻¹
              theorem MonotoneOn.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Preorder β] {f : βα} {s : Set β} (hf : MonotoneOn f s) :
              AntitoneOn (fun (x : β) => -f x) s
              theorem MonotoneOn.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [Preorder β] {f : βα} {s : Set β} (hf : MonotoneOn f s) :
              AntitoneOn (fun (x : β) => (f x)⁻¹) s
              theorem AntitoneOn.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x x_1] [Preorder β] {f : βα} {s : Set β} (hf : AntitoneOn f s) :
              MonotoneOn (fun (x : β) => -f x) s
              theorem AntitoneOn.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x x_1] [Preorder β] {f : βα} {s : Set β} (hf : AntitoneOn f s) :
              MonotoneOn (fun (x : β) => (f x)⁻¹) s
              theorem StrictMono.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [Preorder β] {f : βα} (hf : StrictMono f) :
              StrictAnti fun (x : β) => -f x
              theorem StrictMono.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [Preorder β] {f : βα} (hf : StrictMono f) :
              StrictAnti fun (x : β) => (f x)⁻¹
              theorem StrictAnti.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [Preorder β] {f : βα} (hf : StrictAnti f) :
              StrictMono fun (x : β) => -f x
              theorem StrictAnti.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [Preorder β] {f : βα} (hf : StrictAnti f) :
              StrictMono fun (x : β) => (f x)⁻¹
              theorem StrictMonoOn.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [Preorder β] {f : βα} {s : Set β} (hf : StrictMonoOn f s) :
              StrictAntiOn (fun (x : β) => -f x) s
              theorem StrictMonoOn.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [Preorder β] {f : βα} {s : Set β} (hf : StrictMonoOn f s) :
              StrictAntiOn (fun (x : β) => (f x)⁻¹) s
              theorem StrictAntiOn.neg {α : Type u} {β : Type u_1} [AddGroup α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x < x_1] [Preorder β] {f : βα} {s : Set β} (hf : StrictAntiOn f s) :
              StrictMonoOn (fun (x : β) => -f x) s
              theorem StrictAntiOn.inv {α : Type u} {β : Type u_1} [Group α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x < x_1] [Preorder β] {f : βα} {s : Set β} (hf : StrictAntiOn f s) :
              StrictMonoOn (fun (x : β) => (f x)⁻¹) s