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

class OrderedAddCommGroup (α : Type u) extends , :
• 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 : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = x +
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), = a +
• zsmul_neg' : ∀ (n : ) (a : α), = -SubNegMonoid.zsmul (↑()) 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

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 , :
• 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 : α), = 1
• npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = x *
• inv : αα
• div : ααα
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹
• zpow : αα
• zpow_zero' : ∀ (a : α), = 1
• zpow_succ' : ∀ (n : ) (a : α), = a *
• zpow_neg' : ∀ (n : ) (a : α), = (DivInvMonoid.zpow (↑()) 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

Multiplication is monotone in an ordered commutative group.

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

Instances
theorem OrderedAddCommGroup.to_covariantClass_left_le.proof_1 (α : Type u_1) :
CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1
instance OrderedAddCommGroup.to_covariantClass_left_le (α : Type u) :
CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x x_1
instance OrderedCommGroup.to_covariantClass_left_le (α : Type u) [] :
CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x x_1
theorem OrderedAddCommGroup.toOrderedCancelAddCommMonoid.proof_1 {α : Type u_1} (a : α) (b : α) :
a + b = b + a
theorem OrderedAddCommGroup.toOrderedCancelAddCommMonoid.proof_2 {α : Type u_1} (a : α) (b : α) (c : α) (bc : a + b a + c) :
b c
theorem OrderedAddCommGroup.to_contravariantClass_left_le (α : Type u) :
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) [] :
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) :
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) [] :
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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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
@[simp]
theorem sub_le_sub_iff_right {α : Type u} [] [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
@[simp]
theorem div_le_div_iff_right {α : Type u} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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.

@[simp]
theorem sub_nonpos {α : Type u} [] [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
@[simp]
theorem div_le_one' {α : Type u} [] [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_of_sub_nonpos {α : Type u} [] [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 sub_nonpos_of_le {α : Type u} [] [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_sub_iff_add_le {α : Type u} [] [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} [] [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_sub_right_of_add_le {α : Type u} [] [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 add_le_of_le_sub_right {α : Type u} [] [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 sub_le_iff_le_add {α : Type u} [] [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 div_le_iff_le_mul {α : Type u} [] [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 AddGroup.toHasOrderedSub {α : Type u_1} [] [LE α] [CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1] :
@[simp]
theorem sub_le_sub_iff_left {α : Type u} [] [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
@[simp]
theorem div_le_div_iff_left {α : Type u} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [] [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} [] [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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 sub_pos_of_lt {α : Type u} [] [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.

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

@[simp]
theorem sub_neg {α : Type u} [] [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} [] [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 sub_neg_of_lt {α : Type u} [] [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 lt_of_sub_neg {α : Type u} [] [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_lt_zero {α : Type u} [] [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} [] [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} [] [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_sub_right_of_add_lt {α : Type u} [] [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 add_lt_of_lt_sub_right {α : Type u} [] [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 sub_lt_iff_lt_add {α : Type u} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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 add_lt_of_lt_sub_left {α : Type u} [] [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 lt_sub_left_of_add_lt {α : Type u} [] [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 sub_lt_iff_lt_add' {α : Type u} [] [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} [] [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 sub_left_lt_of_lt_add {α : Type u} [] [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 lt_add_of_sub_left_lt {α : Type u} [] [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 neg_lt_sub_iff_lt_add' {α : Type u} [] [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} [] [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} [] [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} [] [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} [] [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} [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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} [] [] [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 #

class LinearOrderedAddCommGroup (α : Type u) extends , , , :
• 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 : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = x +
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α), = 0
• zsmul_succ' : ∀ (n : ) (a : α), = a +
• zsmul_neg' : ∀ (n : ) (a : α), = -SubNegMonoid.zsmul (↑()) 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 :

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 =

Comparison via compare is equal to the canonical comparison given decidable < and =.

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

Instances
class LinearOrderedAddCommGroupWithTop (α : Type u_1) extends , , , :
Type u_1
• 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
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a
• decidableLE : DecidableRel fun x x_1 => x x_1
• decidableEq :
• decidableLT : DecidableRel fun x x_1 => x < x_1
• min_def : ∀ (a b : α), min a b = if a b then a else b
• max_def : ∀ (a b : α), max a b = if a b then b else a
• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =
• 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 : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = x +
• add_comm : ∀ (a b : α), a + b = b + a
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
• top : α
• le_top : ∀ (x : α), x
• top_add' : ∀ (x : α), + x =
• neg : αα
• sub : ααα
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : αα
• zsmul_zero' : ∀ (a : α),
• zsmul_succ' : ∀ (n : ) (a : α),
• zsmul_neg' : ∀ (n : ) (a : α),
• exists_pair_ne : x y, x y
• neg_top :
• add_neg_cancel : ∀ (a : α), a a + -a = 0

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 , , , :
• 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 : α), = 1
• npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = x *
• inv : αα
• div : ααα
• div_eq_mul_inv : ∀ (a b : α), a / b = a * b⁻¹
• zpow : αα
• zpow_zero' : ∀ (a : α), = 1
• zpow_succ' : ∀ (n : ) (a : α), = a *
• zpow_neg' : ∀ (n : ) (a : α), = (DivInvMonoid.zpow (↑()) 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 :

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 =

Comparison via compare is equal to the canonical comparison given decidable < and =.

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} (a : α) (b : α) (h : a < b) (c : α) :
c + a < c + b
theorem LinearOrderedCommGroup.mul_lt_mul_left' {α : Type u} (a : α) (b : α) (h : a < b) (c : α) :
c * a < c * b
abbrev eq_zero_of_neg_eq.match_1 {α : Type u_1} {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
Instances For
theorem eq_zero_of_neg_eq {α : Type u} {a : α} (h : -a = a) :
a = 0
theorem eq_one_of_inv_eq' {α : Type u} {a : α} (h : a⁻¹ = a) :
a = 1
theorem exists_zero_lt {α : Type u} [] :
a, 0 < a
theorem exists_one_lt' {α : Type u} [] :
a, 1 < a
theorem LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid.proof_1 {α : Type u_1} (a : α) (b : α) :
a b∀ (c : α), c + a c + b
structure AddCommGroup.PositiveCone (α : Type u_1) [] :
Type u_1
• nonneg : αProp
• pos : αProp
• pos_iff : ∀ (a : α),
• zero_nonneg :
• add_nonneg : ∀ {a b : α},
• nonneg_antisymm : ∀ {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 existing AddCommGroup.

Instances For
structure AddCommGroup.TotalPositiveCone (α : Type u_1) [] extends :
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
def OrderedAddCommGroup.mkOfPositiveCone {α : Type u_1} [] (C : ) :

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

Instances For

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

Instances For
theorem neg_le_neg {α : Type u} {a : α} {b : α} :
a b-b -a
theorem inv_le_inv' {α : Type u} [] {a : α} {b : α} :
a bb⁻¹ a⁻¹
theorem neg_lt_neg {α : Type u} {a : α} {b : α} :
a < b-b < -a
theorem inv_lt_inv' {α : Type u} [] {a : α} {b : α} :
a < bb⁻¹ < a⁻¹
theorem neg_neg_of_pos {α : Type u} {a : α} :
0 < a-a < 0
theorem inv_lt_one_of_one_lt {α : Type u} [] {a : α} :
1 < aa⁻¹ < 1
theorem neg_nonpos_of_nonneg {α : Type u} {a : α} :
0 a-a 0
theorem inv_le_one_of_one_le {α : Type u} [] {a : α} :
1 aa⁻¹ 1
theorem neg_nonneg_of_nonpos {α : Type u} {a : α} :
a 00 -a
theorem one_le_inv_of_le_one {α : Type u} [] {a : α} :
a 11 a⁻¹
theorem Monotone.neg {α : Type u} {β : Type u_1} [] [] [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] [] {f : βα} (hf : ) :
Antitone fun x => -f x
theorem Monotone.inv {α : Type u} {β : Type u_1} [] [] [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] [] {f : βα} (hf : ) :
Antitone fun x => (f x)⁻¹
theorem Antitone.neg {α : Type u} {β : Type u_1} [] [] [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] [] {f : βα} (hf : ) :
Monotone fun x => -f x
theorem Antitone.inv {α : Type u} {β : Type u_1} [] [] [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] [] {f : βα} (hf : ) :
Monotone fun x => (f x)⁻¹
theorem MonotoneOn.neg {α : Type u} {β : Type u_1} [] [] [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] [] {f : βα} {s : Set β} (hf : ) :
AntitoneOn (fun x => -f x) s
theorem MonotoneOn.inv {α : Type u} {β : Type u_1} [] [] [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] [] {f : βα} {s : Set β} (hf : ) :
AntitoneOn (fun x => (f x)⁻¹) s
theorem AntitoneOn.neg {α : Type u} {β : Type u_1} [] [] [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] [] {f : βα} {s : Set β} (hf : ) :
MonotoneOn (fun x => -f x) s
theorem AntitoneOn.inv {α : Type u} {β : Type u_1} [] [] [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] [] {f : βα} {s : Set β} (hf : ) :
MonotoneOn (fun x => (f x)⁻¹) s
theorem StrictMono.neg {α : Type u} {β : Type u_1} [] [] [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] [] {f : βα} (hf : ) :
StrictAnti fun x => -f x
theorem StrictMono.inv {α : Type u} {β : Type u_1} [] [] [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] [] {f : βα} (hf : ) :
StrictAnti fun x => (f x)⁻¹
theorem StrictAnti.neg {α : Type u} {β : Type u_1} [] [] [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] [] {f : βα} (hf : ) :
StrictMono fun x => -f x
theorem StrictAnti.inv {α : Type u} {β : Type u_1} [] [] [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] [] {f : βα} (hf : ) :
StrictMono fun x => (f x)⁻¹
theorem StrictMonoOn.neg {α : Type u} {β : Type u_1} [] [] [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] [] {f : βα} {s : Set β} (hf : ) :
StrictAntiOn (fun x => -f x) s
theorem StrictMonoOn.inv {α : Type u} {β : Type u_1} [] [] [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] [] {f : βα} {s : Set β} (hf : ) :
StrictAntiOn (fun x => (f x)⁻¹) s
theorem StrictAntiOn.neg {α : Type u} {β : Type u_1} [] [] [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] [] {f : βα} {s : Set β} (hf : ) :
StrictMonoOn (fun x => -f x) s
theorem StrictAntiOn.inv {α : Type u} {β : Type u_1} [] [] [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] [] {f : βα} {s : Set β} (hf : ) :
StrictMonoOn (fun x => (f x)⁻¹) s