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 AddCommGroup , PartialOrder : Type u

An ordered additive commutative group is an additive commutative group with a partial order in which addition is strictly 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 = x + AddMonoid.nsmul n 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 (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• add_le_add_left : ∀ (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 : Type u

An ordered commutative group is a commutative group with a partial order in which multiplication is strictly 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 = x * Monoid.npow n 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 (Nat.succ n)) a = a * DivInvMonoid.zpow (Int.ofNat n) a
• zpow_neg' : ∀ (n : ℕ) (a : α), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑(Nat.succ n)) 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• mul_le_mul_left : ∀ (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

• (_ : CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1) = (_ : CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1)

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

• (_ : CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1) = (_ : CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1)

theorem OrderedAddCommGroup.toOrderedCancelAddCommMonoid.proof_2 {α : Type u_1} [OrderedAddCommGroup α] (a : α) (b : α) (c : α) (bc : a + b ≤ a + c) : b ≤ c

instance OrderedAddCommGroup.toOrderedCancelAddCommMonoid {α : Type u} [OrderedAddCommGroup α] : OrderedCancelAddCommMonoid α

Equations

• OrderedAddCommGroup.toOrderedCancelAddCommMonoid = let src := inst; OrderedCancelAddCommMonoid.mk (_ : ∀ (a b c : α), a + b ≤ a + c → b ≤ c)

theorem OrderedAddCommGroup.toOrderedCancelAddCommMonoid.proof_1 {α : Type u_1} [OrderedAddCommGroup α] (a : α) (b : α) : a + b = b + a

instance OrderedCommGroup.toOrderedCancelCommMonoid {α : Type u} [OrderedCommGroup α] : OrderedCancelCommMonoid α

Equations

• OrderedCommGroup.toOrderedCancelCommMonoid = let src := inst; OrderedCancelCommMonoid.mk (_ : ∀ (a b c : α), a * b ≤ a * c → b ≤ c)

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 : α} : a⁻¹ ≤ b⁻¹ ↔ b ≤ a

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 ≤ -b → b ≤ 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 ≤ b → a - 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 < -b → b < -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⁻¹ < b → b⁻¹ < 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 < b → a - 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) : a⁻¹ ≤ 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) : a ≤ a⁻¹

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) : a⁻¹ ≤ 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) : a ≤ a⁻¹

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⁻¹ ≤ 1 → 1 ≤ 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 ≤ 0 → 0 ≤ 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 ≤ -a → a ≤ 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 < -b → b < 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⁻¹ < 1 → 1 < 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 < 0 → 0 < 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 < -a → a < 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 < 1 → 1 < 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 < 0 → 0 < -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⁻¹ * c → a * 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 + c → a + 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 ≤ c → b ≤ 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 ≤ c → b ≤ -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 * c → b⁻¹ * 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⁻¹ * c → a * 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 + c → a + 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 < c → b < 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 < c → b < -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 < c → a < 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 * c → b⁻¹ * 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 < c → a < 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 < c → a < 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 < c → a < 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 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 - b → b ≤ a

Alias of the forward direction of sub_nonneg.

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 ≤ a → 0 ≤ a - b

Alias of the reverse 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 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 ≤ 0 → a ≤ b

Alias of the forward direction of sub_nonpos.

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 ≤ b → a - b ≤ 0

Alias of the reverse 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 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 ≤ c → a ≤ c - b

Alias of the reverse direction of le_sub_iff_add_le.

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 - b → a + b ≤ c

Alias of the forward 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 AddGroup.toHasOrderedSub {α : Type u_1} [AddGroup α] [LE α] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] : OrderedSub α

Equations

• (_ : OrderedSub α) = (_ : OrderedSub α)

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 ≤ c → b ≤ 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 - a → a + 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 + c → a - 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 ≤ c → a ≤ 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 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 < a → 0 < a - b

Alias of the reverse direction of sub_pos.

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 - b → b < a

Alias of the forward 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 < 0 → a < 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 < b → a - 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 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 < c → a < c - b

Alias of the reverse direction of lt_sub_iff_add_lt.

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 - b → a + b < c

Alias of the forward 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 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 + c → a - c < b

Alias of the reverse direction of sub_lt_iff_lt_add.

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 < b → a < b + c

Alias of the forward 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 < c → b < 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 - a → a + 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 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 + c → a - b < c

Alias of the reverse direction of sub_lt_iff_lt_add'.

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 < c → a < b + c

Alias of the forward 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 - c → a < 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 / c → a < 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

class LinearOrderedAddCommGroup (α : Type u) extends OrderedAddCommGroup , Min , Max , Ord : Type u

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 = x + AddMonoid.nsmul n 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 (Nat.succ n)) a = a + SubNegMonoid.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), SubNegMonoid.zsmul (Int.negSucc n) a = -SubNegMonoid.zsmul (↑(Nat.succ n)) 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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 =.

class LinearOrderedAddCommGroupWithTop (α : Type u_1) extends LinearOrderedAddCommMonoidWithTop , Neg , Sub , Nontrivial : Type u_1

A linearly ordered commutative group with an additively absorbing ⊤ element. Instances should include number systems with an infinite element adjoined.

• 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 = x + AddMonoid.nsmul n x
• add_comm : ∀ (a b : α), a + b = b + a
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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
• decidableLE : DecidableRel fun (x x_1 : α) => x ≤ x_1
• decidableEq : 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 = compareOfLessAndEq a b
• top : α
• le_top : ∀ (a : α), a ≤ ⊤
• top_add' : ∀ (x : α), ⊤ + x = ⊤
• neg : α → α
• sub : α → α → α
• sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
• zsmul : ℤ → α → α
• zsmul_zero' : ∀ (a : α), LinearOrderedAddCommGroupWithTop.zsmul 0 a = 0
• zsmul_succ' : ∀ (n : ℕ) (a : α), LinearOrderedAddCommGroupWithTop.zsmul (Int.ofNat (Nat.succ n)) a = a + LinearOrderedAddCommGroupWithTop.zsmul (Int.ofNat n) a
• zsmul_neg' : ∀ (n : ℕ) (a : α), LinearOrderedAddCommGroupWithTop.zsmul (Int.negSucc n) a = -LinearOrderedAddCommGroupWithTop.zsmul (↑(Nat.succ n)) a
• exists_pair_ne : ∃ (x : α), ∃ (y : α), x ≠ y
• neg_top : -⊤ = ⊤
• add_neg_cancel : ∀ (a : α), a ≠ ⊤ → a + -a = 0

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

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 = x * Monoid.npow n 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 (Nat.succ n)) a = a * DivInvMonoid.zpow (Int.ofNat n) a
• zpow_neg' : ∀ (n : ℕ) (a : α), DivInvMonoid.zpow (Int.negSucc n) a = (DivInvMonoid.zpow (↑(Nat.succ n)) 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = 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 =.

theorem LinearOrderedAddCommGroup.add_lt_add_left {α : Type u} [LinearOrderedAddCommGroup α] (a : α) (b : α) (h : a < b) (c : α) : c + a < c + b

theorem LinearOrderedCommGroup.mul_lt_mul_left' {α : Type u} [LinearOrderedCommGroup α] (a : α) (b : α) (h : a < b) (c : α) : c * a < c * b

theorem eq_zero_of_neg_eq {α : Type u} [LinearOrderedAddCommGroup α] {a : α} (h : -a = a) : a = 0

abbrev eq_zero_of_neg_eq.match_1 {α : Type u_1} [LinearOrderedAddCommGroup α] {a : α} (motive : a < 0 ∨ a = 0 ∨ 0 < a → Prop) : ∀ (x : a < 0 ∨ a = 0 ∨ 0 < a), (∀ (h₁ : a < 0), motive (_ : a < 0 ∨ a = 0 ∨ 0 < a)) → (∀ (h₁ : a = 0), motive (_ : a < 0 ∨ a = 0 ∨ 0 < a)) → (∀ (h₁ : 0 < a), motive (_ : a < 0 ∨ a = 0 ∨ 0 < a)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

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 LinearOrderedAddCommGroup.to_noMaxOrder {α : Type u} [LinearOrderedAddCommGroup α] [Nontrivial α] : NoMaxOrder α

Equations

• (_ : NoMaxOrder α) = (_ : NoMaxOrder α)

instance LinearOrderedCommGroup.to_noMaxOrder {α : Type u} [LinearOrderedCommGroup α] [Nontrivial α] : NoMaxOrder α

Equations

• (_ : NoMaxOrder α) = (_ : NoMaxOrder α)

instance LinearOrderedAddCommGroup.to_noMinOrder {α : Type u} [LinearOrderedAddCommGroup α] [Nontrivial α] : NoMinOrder α

Equations

• (_ : NoMinOrder α) = (_ : NoMinOrder α)

instance LinearOrderedCommGroup.to_noMinOrder {α : Type u} [LinearOrderedCommGroup α] [Nontrivial α] : NoMinOrder α

Equations

• (_ : NoMinOrder α) = (_ : NoMinOrder α)

instance LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid {α : Type u} [LinearOrderedAddCommGroup α] : LinearOrderedCancelAddCommMonoid α

Equations

• One or more equations did not get rendered due to their size.

theorem LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid.proof_1 {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) : a + b = b + a

theorem LinearOrderedAddCommGroup.toLinearOrderedAddCancelCommMonoid.proof_2 {α : Type u_1} [LinearOrderedAddCommGroup α] (a : α) (b : α) : a ≤ b → ∀ (c : α), c + a ≤ c + b

instance LinearOrderedCommGroup.toLinearOrderedCancelCommMonoid {α : Type u} [LinearOrderedCommGroup α] : LinearOrderedCancelCommMonoid α

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

structure AddCommGroup.PositiveCone (α : Type u_1) [AddCommGroup α] : Type u_1

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.

• nonneg : α → Prop

  The characteristic predicate of a positive cone. nonneg a means that 0 ≤ a according to the cone.

• pos : α → Prop

  The characteristic predicate of a positive cone. pos a means that 0 < a according to the cone.

• pos_iff : ∀ (a : α), self.pos a ↔ self.nonneg a ∧ ¬self.nonneg (-a)
• zero_nonneg : self.nonneg 0
• add_nonneg : ∀ {a b : α}, self.nonneg a → self.nonneg b → self.nonneg (a + b)
• nonneg_antisymm : ∀ {a : α}, self.nonneg a → self.nonneg (-a) → a = 0

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

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

• nonneg : α → Prop
• pos : α → Prop
• pos_iff : ∀ (a : α), self.toPositiveCone.pos a ↔ self.toPositiveCone.nonneg a ∧ ¬self.toPositiveCone.nonneg (-a)
• zero_nonneg : self.toPositiveCone.nonneg 0
• add_nonneg : ∀ {a b : α}, self.toPositiveCone.nonneg a → self.toPositiveCone.nonneg b → self.toPositiveCone.nonneg (a + b)
• nonneg_antisymm : ∀ {a : α}, self.toPositiveCone.nonneg a → self.toPositiveCone.nonneg (-a) → a = 0
• nonnegDecidable : DecidablePred self.nonneg

  For any a the proposition nonneg a is decidable

• nonneg_total : ∀ (a : α), self.toPositiveCone.nonneg a ∨ self.toPositiveCone.nonneg (-a)

  Either a or -a is nonneg

def OrderedAddCommGroup.mkOfPositiveCone {α : Type u_1} [AddCommGroup α] (C : AddCommGroup.PositiveCone α) : OrderedAddCommGroup α

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

Equations

• OrderedAddCommGroup.mkOfPositiveCone C = let src := inst; OrderedAddCommGroup.mk (_ : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b)

def LinearOrderedAddCommGroup.mkOfPositiveCone {α : Type u_1} [AddCommGroup α] (C : AddCommGroup.TotalPositiveCone α) : LinearOrderedAddCommGroup α

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

Equations

• One or more equations did not get rendered due to their size.

theorem neg_le_neg {α : Type u} [OrderedAddCommGroup α] {a : α} {b : α} : a ≤ b → -b ≤ -a

theorem inv_le_inv' {α : Type u} [OrderedCommGroup α] {a : α} {b : α} : a ≤ b → b⁻¹ ≤ a⁻¹

theorem neg_lt_neg {α : Type u} [OrderedAddCommGroup α] {a : α} {b : α} : a < b → -b < -a

theorem inv_lt_inv' {α : Type u} [OrderedCommGroup α] {a : α} {b : α} : a < b → b⁻¹ < 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 < a → a⁻¹ < 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 ≤ a → a⁻¹ ≤ 1

theorem neg_nonneg_of_nonpos {α : Type u} [OrderedAddCommGroup α] {a : α} : a ≤ 0 → 0 ≤ -a

theorem one_le_inv_of_le_one {α : Type u} [OrderedCommGroup α] {a : α} : a ≤ 1 → 1 ≤ 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