mathlib documentation

algebra.ordered_group

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]
structure ordered_add_comm_group (α : Type u) :
Type u
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • neg : α → α
  • sub : α → α → α
  • sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
  • 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_1 : α), a bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • add_le_add_left : ∀ (a b : α), a b∀ (c_1 : α), c_1 + a c_1 + b

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

Instances
@[instance]

@[class]
structure ordered_comm_group (α : Type u) :
Type u
  • mul : α → α → α
  • mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • inv : α → α
  • div : α → α → α
  • div_eq_mul_inv : (∀ (a b : α), a / b = a * b⁻¹) . "try_refl_tac"
  • 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_1 : α), a bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • mul_le_mul_left : ∀ (a b : α), a b∀ (c_1 : α), c_1 * a c_1 * b

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

Instances
@[instance]

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

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

theorem ordered_add_comm_group.le_of_add_le_add_left {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a + b a + c) :
b c

theorem ordered_comm_group.le_of_mul_le_mul_left {α : Type u} [ordered_comm_group α] {a b c : α} (h : a * b a * c) :
b c

theorem ordered_comm_group.lt_of_mul_lt_mul_left {α : Type u} [ordered_comm_group α] {a b c : α} (h : a * b < a * c) :
b < c

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

theorem neg_le_neg {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a b) :
-b -a

theorem inv_le_inv' {α : Type u} [ordered_comm_group α] {a b : α} (h : a b) :

theorem le_of_neg_le_neg {α : Type u} [ordered_add_comm_group α] {a b : α} (h : -b -a) :
a b

theorem le_of_inv_le_inv {α : Type u} [ordered_comm_group α] {a b : α} (h : b⁻¹ a⁻¹) :
a b

theorem one_le_of_inv_le_one {α : Type u} [ordered_comm_group α] {a : α} (h : a⁻¹ 1) :
1 a

theorem nonneg_of_neg_nonpos {α : Type u} [ordered_add_comm_group α] {a : α} (h : -a 0) :
0 a

theorem inv_le_one_of_one_le {α : Type u} [ordered_comm_group α] {a : α} (h : 1 a) :

theorem neg_nonpos_of_nonneg {α : Type u} [ordered_add_comm_group α] {a : α} (h : 0 a) :
-a 0

theorem le_one_of_one_le_inv {α : Type u} [ordered_comm_group α] {a : α} (h : 1 a⁻¹) :
a 1

theorem nonpos_of_neg_nonneg {α : Type u} [ordered_add_comm_group α] {a : α} (h : 0 -a) :
a 0

theorem one_le_inv_of_le_one {α : Type u} [ordered_comm_group α] {a : α} (h : a 1) :

theorem neg_nonneg_of_nonpos {α : Type u} [ordered_add_comm_group α] {a : α} (h : a 0) :
0 -a

theorem neg_lt_neg {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a < b) :
-b < -a

theorem inv_lt_inv' {α : Type u} [ordered_comm_group α] {a b : α} (h : a < b) :

theorem lt_of_inv_lt_inv {α : Type u} [ordered_comm_group α] {a b : α} (h : b⁻¹ < a⁻¹) :
a < b

theorem lt_of_neg_lt_neg {α : Type u} [ordered_add_comm_group α] {a b : α} (h : -b < -a) :
a < b

theorem pos_of_neg_neg {α : Type u} [ordered_add_comm_group α] {a : α} (h : -a < 0) :
0 < a

theorem one_lt_of_inv_inv {α : Type u} [ordered_comm_group α] {a : α} (h : a⁻¹ < 1) :
1 < a

theorem inv_inv_of_one_lt {α : Type u} [ordered_comm_group α] {a : α} (h : 1 < a) :
a⁻¹ < 1

theorem neg_neg_of_pos {α : Type u} [ordered_add_comm_group α] {a : α} (h : 0 < a) :
-a < 0

theorem neg_of_neg_pos {α : Type u} [ordered_add_comm_group α] {a : α} (h : 0 < -a) :
a < 0

theorem inv_of_one_lt_inv {α : Type u} [ordered_comm_group α] {a : α} (h : 1 < a⁻¹) :
a < 1

theorem one_lt_inv_of_inv {α : Type u} [ordered_comm_group α] {a : α} (h : a < 1) :
1 < a⁻¹

theorem neg_pos_of_neg {α : Type u} [ordered_add_comm_group α] {a : α} (h : a < 0) :
0 < -a

theorem le_neg_of_le_neg {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a -b) :
b -a

theorem le_inv_of_le_inv {α : Type u} [ordered_comm_group α] {a b : α} (h : a b⁻¹) :

theorem inv_le_of_inv_le {α : Type u} [ordered_comm_group α] {a b : α} (h : a⁻¹ b) :

theorem neg_le_of_neg_le {α : Type u} [ordered_add_comm_group α] {a b : α} (h : -a b) :
-b a

theorem lt_neg_of_lt_neg {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a < -b) :
b < -a

theorem lt_inv_of_lt_inv {α : Type u} [ordered_comm_group α] {a b : α} (h : a < b⁻¹) :
b < a⁻¹

theorem inv_lt_of_inv_lt {α : Type u} [ordered_comm_group α] {a b : α} (h : a⁻¹ < b) :
b⁻¹ < a

theorem neg_lt_of_neg_lt {α : Type u} [ordered_add_comm_group α] {a b : α} (h : -a < b) :
-b < a

theorem add_le_of_le_neg_add {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : b -a + c) :
a + b c

theorem mul_le_of_le_inv_mul {α : Type u} [ordered_comm_group α] {a b c : α} (h : b a⁻¹ * c) :
a * b c

theorem le_inv_mul_of_mul_le {α : Type u} [ordered_comm_group α] {a b c : α} (h : a * b c) :
b a⁻¹ * c

theorem le_neg_add_of_add_le {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a + b c) :
b -a + c

theorem le_mul_of_inv_mul_le {α : Type u} [ordered_comm_group α] {a b c : α} (h : b⁻¹ * a c) :
a b * c

theorem le_add_of_neg_add_le {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : -b + a c) :
a b + c

theorem neg_add_le_of_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a b + c) :
-b + a c

theorem inv_mul_le_of_le_mul {α : Type u} [ordered_comm_group α] {a b c : α} (h : a b * c) :
b⁻¹ * a c

theorem le_mul_of_inv_mul_le_left {α : Type u} [ordered_comm_group α] {a b c : α} (h : b⁻¹ * a c) :
a b * c

theorem le_add_of_neg_add_le_left {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : -b + a c) :
a b + c

theorem neg_add_le_left_of_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a b + c) :
-b + a c

theorem inv_mul_le_left_of_le_mul {α : Type u} [ordered_comm_group α] {a b c : α} (h : a b * c) :
b⁻¹ * a c

theorem le_mul_of_inv_mul_le_right {α : Type u} [ordered_comm_group α] {a b c : α} (h : c⁻¹ * a b) :
a b * c

theorem le_add_of_neg_add_le_right {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : -c + a b) :
a b + c

theorem neg_add_le_right_of_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a b + c) :
-c + a b

theorem inv_mul_le_right_of_le_mul {α : Type u} [ordered_comm_group α] {a b c : α} (h : a b * c) :
c⁻¹ * a b

theorem add_lt_of_lt_neg_add {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : b < -a + c) :
a + b < c

theorem mul_lt_of_lt_inv_mul {α : Type u} [ordered_comm_group α] {a b c : α} (h : b < a⁻¹ * c) :
a * b < c

theorem lt_inv_mul_of_mul_lt {α : Type u} [ordered_comm_group α] {a b c : α} (h : a * b < c) :
b < a⁻¹ * c

theorem lt_neg_add_of_add_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a + b < c) :
b < -a + c

theorem lt_add_of_neg_add_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : -b + a < c) :
a < b + c

theorem lt_mul_of_inv_mul_lt {α : Type u} [ordered_comm_group α] {a b c : α} (h : b⁻¹ * a < c) :
a < b * c

theorem neg_add_lt_of_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a < b + c) :
-b + a < c

theorem inv_mul_lt_of_lt_mul {α : Type u} [ordered_comm_group α] {a b c : α} (h : a < b * c) :
b⁻¹ * a < c

theorem lt_add_of_neg_add_lt_left {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : -b + a < c) :
a < b + c

theorem lt_mul_of_inv_mul_lt_left {α : Type u} [ordered_comm_group α] {a b c : α} (h : b⁻¹ * a < c) :
a < b * c

theorem inv_mul_lt_left_of_lt_mul {α : Type u} [ordered_comm_group α] {a b c : α} (h : a < b * c) :
b⁻¹ * a < c

theorem neg_add_lt_left_of_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a < b + c) :
-b + a < c

theorem lt_add_of_neg_add_lt_right {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : -c + a < b) :
a < b + c

theorem lt_mul_of_inv_mul_lt_right {α : Type u} [ordered_comm_group α] {a b c : α} (h : c⁻¹ * a < b) :
a < b * c

theorem inv_mul_lt_right_of_lt_mul {α : Type u} [ordered_comm_group α] {a b c : α} (h : a < b * c) :
c⁻¹ * a < b

theorem neg_add_lt_right_of_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a < b + c) :
-c + a < b

@[simp]
theorem inv_lt_one_iff_one_lt {α : Type u} [ordered_comm_group α] {a : α} :
a⁻¹ < 1 1 < a

@[simp]
theorem neg_neg_iff_pos {α : Type u} [ordered_add_comm_group α] {a : α} :
-a < 0 0 < a

@[simp]
theorem neg_le_neg_iff {α : Type u} [ordered_add_comm_group α] {a b : α} :
-a -b b a

@[simp]
theorem inv_le_inv_iff {α : Type u} [ordered_comm_group α] {a b : α} :

theorem neg_le {α : Type u} [ordered_add_comm_group α] {a b : α} :
-a b -b a

theorem inv_le' {α : Type u} [ordered_comm_group α] {a b : α} :

theorem le_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :
a -b b -a

theorem le_inv' {α : Type u} [ordered_comm_group α] {a b : α} :

theorem inv_le_iff_one_le_mul {α : Type u} [ordered_comm_group α] {a b : α} :
a⁻¹ b 1 b * a

theorem neg_le_iff_add_nonneg {α : Type u} [ordered_add_comm_group α] {a b : α} :
-a b 0 b + a

theorem inv_le_iff_one_le_mul' {α : Type u} [ordered_comm_group α] {a b : α} :
a⁻¹ b 1 a * b

theorem neg_le_iff_add_nonneg' {α : Type u} [ordered_add_comm_group α] {a b : α} :
-a b 0 a + b

theorem neg_lt_iff_pos_add {α : Type u} [ordered_add_comm_group α] {a b : α} :
-a < b 0 < b + a

theorem inv_lt_iff_one_lt_mul {α : Type u} [ordered_comm_group α] {a b : α} :
a⁻¹ < b 1 < b * a

theorem inv_lt_iff_one_lt_mul' {α : Type u} [ordered_comm_group α] {a b : α} :
a⁻¹ < b 1 < a * b

theorem neg_lt_iff_pos_add' {α : Type u} [ordered_add_comm_group α] {a b : α} :
-a < b 0 < a + b

theorem le_neg_iff_add_nonpos {α : Type u} [ordered_add_comm_group α] {a b : α} :
a -b a + b 0

theorem le_inv_iff_mul_le_one {α : Type u} [ordered_comm_group α] {a b : α} :
a b⁻¹ a * b 1

theorem le_inv_iff_mul_le_one' {α : Type u} [ordered_comm_group α] {a b : α} :
a b⁻¹ b * a 1

theorem le_neg_iff_add_nonpos' {α : Type u} [ordered_add_comm_group α] {a b : α} :
a -b b + a 0

theorem lt_inv_iff_mul_lt_one {α : Type u} [ordered_comm_group α] {a b : α} :
a < b⁻¹ a * b < 1

theorem lt_neg_iff_add_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :
a < -b a + b < 0

theorem lt_inv_iff_mul_lt_one' {α : Type u} [ordered_comm_group α] {a b : α} :
a < b⁻¹ b * a < 1

theorem lt_neg_iff_add_neg' {α : Type u} [ordered_add_comm_group α] {a b : α} :
a < -b b + a < 0

@[simp]
theorem neg_nonpos {α : Type u} [ordered_add_comm_group α] {a : α} :
-a 0 0 a

@[simp]
theorem inv_le_one' {α : Type u} [ordered_comm_group α] {a : α} :
a⁻¹ 1 1 a

@[simp]
theorem one_le_inv' {α : Type u} [ordered_comm_group α] {a : α} :
1 a⁻¹ a 1

@[simp]
theorem neg_nonneg {α : Type u} [ordered_add_comm_group α] {a : α} :
0 -a a 0

theorem inv_le_self {α : Type u} [ordered_comm_group α] {a : α} (h : 1 a) :

theorem neg_le_self {α : Type u} [ordered_add_comm_group α] {a : α} (h : 0 a) :
-a a

theorem self_le_inv {α : Type u} [ordered_comm_group α] {a : α} (h : a 1) :

theorem self_le_neg {α : Type u} [ordered_add_comm_group α] {a : α} (h : a 0) :
a -a

@[simp]
theorem inv_lt_inv_iff {α : Type u} [ordered_comm_group α] {a b : α} :
a⁻¹ < b⁻¹ b < a

@[simp]
theorem neg_lt_neg_iff {α : Type u} [ordered_add_comm_group α] {a b : α} :
-a < -b b < a

theorem inv_lt_one' {α : Type u} [ordered_comm_group α] {a : α} :
a⁻¹ < 1 1 < a

theorem neg_lt_zero {α : Type u} [ordered_add_comm_group α] {a : α} :
-a < 0 0 < a

theorem neg_pos {α : Type u} [ordered_add_comm_group α] {a : α} :
0 < -a a < 0

theorem one_lt_inv' {α : Type u} [ordered_comm_group α] {a : α} :
1 < a⁻¹ a < 1

theorem neg_lt {α : Type u} [ordered_add_comm_group α] {a b : α} :
-a < b -b < a

theorem inv_lt' {α : Type u} [ordered_comm_group α] {a b : α} :
a⁻¹ < b b⁻¹ < a

theorem lt_inv' {α : Type u} [ordered_comm_group α] {a b : α} :
a < b⁻¹ b < a⁻¹

theorem lt_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :
a < -b b < -a

theorem neg_lt_self {α : Type u} [ordered_add_comm_group α] {a : α} (h : 0 < a) :
-a < a

theorem inv_lt_self {α : Type u} [ordered_comm_group α] {a : α} (h : 1 < a) :
a⁻¹ < a

theorem le_neg_add_iff_add_le {α : Type u} [ordered_add_comm_group α] {a b c : α} :
b -a + c a + b c

theorem le_inv_mul_iff_mul_le {α : Type u} [ordered_comm_group α] {a b c : α} :
b a⁻¹ * c a * b c

@[simp]
theorem inv_mul_le_iff_le_mul {α : Type u} [ordered_comm_group α] {a b c : α} :
b⁻¹ * a c a b * c

@[simp]
theorem neg_add_le_iff_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :
-b + a c a b + c

theorem mul_inv_le_iff_le_mul {α : Type u} [ordered_comm_group α] {a b c : α} :
a * c⁻¹ b a b * c

theorem add_neg_le_iff_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a + -c b a b + c

@[simp]
theorem mul_inv_le_iff_le_mul' {α : Type u} [ordered_comm_group α] {a b c : α} :
a * b⁻¹ c a b * c

@[simp]
theorem add_neg_le_iff_le_add' {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a + -b c a b + c

theorem inv_mul_le_iff_le_mul' {α : Type u} [ordered_comm_group α] {a b c : α} :
c⁻¹ * a b a b * c

theorem neg_add_le_iff_le_add' {α : Type u} [ordered_add_comm_group α] {a b c : α} :
-c + a b a b + c

@[simp]
theorem lt_inv_mul_iff_mul_lt {α : Type u} [ordered_comm_group α] {a b c : α} :
b < a⁻¹ * c a * b < c

@[simp]
theorem lt_neg_add_iff_add_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :
b < -a + c a + b < c

@[simp]
theorem inv_mul_lt_iff_lt_mul {α : Type u} [ordered_comm_group α] {a b c : α} :
b⁻¹ * a < c a < b * c

@[simp]
theorem neg_add_lt_iff_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :
-b + a < c a < b + c

theorem neg_add_lt_iff_lt_add_right {α : Type u} [ordered_add_comm_group α] {a b c : α} :
-c + a < b a < b + c

theorem inv_mul_lt_iff_lt_mul_right {α : Type u} [ordered_comm_group α] {a b c : α} :
c⁻¹ * a < b a < b * c

theorem div_le_div_iff' {α : Type u} [ordered_comm_group α] {a b c d : α} :
a * b⁻¹ c * d⁻¹ a * d c * b

theorem add_neg_le_add_neg_iff {α : Type u} [ordered_add_comm_group α] {a b c d : α} :
a + -b c + -d a + d c + b

theorem sub_le_sub {α : Type u} [ordered_add_comm_group α] {a b c d : α} (hab : a b) (hcd : c d) :
a - d b - c

theorem sub_lt_sub {α : Type u} [ordered_add_comm_group α] {a b c d : α} (hab : a < b) (hcd : c < d) :
a - d < b - c

@[simp]
theorem sub_le_self_iff {α : Type u} [ordered_add_comm_group α] (a : α) {b : α} :
a - b a 0 b

theorem sub_le_self {α : Type u} [ordered_add_comm_group α] (a : α) {b : α} :
0 ba - b a

Alias of sub_le_self_iff.

@[simp]
theorem sub_lt_self_iff {α : Type u} [ordered_add_comm_group α] (a : α) {b : α} :
a - b < a 0 < b

theorem sub_lt_self {α : Type u} [ordered_add_comm_group α] (a : α) {b : α} :
0 < ba - b < a

Alias of sub_lt_self_iff.

theorem sub_le_sub_iff {α : Type u} [ordered_add_comm_group α] {a b c d : α} :
a - b c - d a + d c + b

@[simp]
theorem sub_le_sub_iff_left {α : Type u} [ordered_add_comm_group α] (a : α) {b c : α} :
a - b a - c c b

theorem sub_le_sub_left {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a b) (c : α) :
c - b c - a

@[simp]
theorem sub_le_sub_iff_right {α : Type u} [ordered_add_comm_group α] {a b : α} (c : α) :
a - c b - c a b

theorem sub_le_sub_right {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a b) (c : α) :
a - c b - c

@[simp]
theorem sub_lt_sub_iff_left {α : Type u} [ordered_add_comm_group α] (a : α) {b c : α} :
a - b < a - c c < b

theorem sub_lt_sub_left {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a < b) (c : α) :
c - b < c - a

@[simp]
theorem sub_lt_sub_iff_right {α : Type u} [ordered_add_comm_group α] {a b : α} (c : α) :
a - c < b - c a < b

theorem sub_lt_sub_right {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a < b) (c : α) :
a - c < b - c

@[simp]
theorem sub_nonneg {α : Type u} [ordered_add_comm_group α] {a b : α} :
0 a - b b a

theorem le_of_sub_nonneg {α : Type u} [ordered_add_comm_group α] {a b : α} :
0 a - bb a

Alias of sub_nonneg.

theorem sub_nonneg_of_le {α : Type u} [ordered_add_comm_group α] {a b : α} :
b a0 a - b

Alias of sub_nonneg.

@[simp]
theorem sub_nonpos {α : Type u} [ordered_add_comm_group α] {a b : α} :
a - b 0 a b

theorem sub_nonpos_of_le {α : Type u} [ordered_add_comm_group α] {a b : α} :
a ba - b 0

Alias of sub_nonpos.

theorem le_of_sub_nonpos {α : Type u} [ordered_add_comm_group α] {a b : α} :
a - b 0a b

Alias of sub_nonpos.

@[simp]
theorem sub_pos {α : Type u} [ordered_add_comm_group α] {a b : α} :
0 < a - b b < a

theorem lt_of_sub_pos {α : Type u} [ordered_add_comm_group α] {a b : α} :
0 < a - bb < a

Alias of sub_pos.

theorem sub_pos_of_lt {α : Type u} [ordered_add_comm_group α] {a b : α} :
b < a0 < a - b

Alias of sub_pos.

@[simp]
theorem sub_lt_zero {α : Type u} [ordered_add_comm_group α] {a b : α} :
a - b < 0 a < b

theorem lt_of_sub_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :
a - b < 0a < b

Alias of sub_lt_zero.

theorem sub_neg_of_lt {α : Type u} [ordered_add_comm_group α] {a b : α} :
a < ba - b < 0

Alias of sub_lt_zero.

theorem le_sub_iff_add_le' {α : Type u} [ordered_add_comm_group α] {a b c : α} :
b c - a a + b c

theorem le_sub_iff_add_le {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a c - b a + b c

theorem add_le_of_le_sub_right {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a c - ba + b c

Alias of le_sub_iff_add_le.

theorem le_sub_right_of_add_le {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a + b ca c - b

Alias of le_sub_iff_add_le.

theorem sub_le_iff_le_add' {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a - b c a b + c

theorem add_le_of_le_sub_left {α : Type u} [ordered_add_comm_group α] {a b c : α} :
b c - aa + b c

Alias of le_sub_iff_add_le'.

theorem le_sub_left_of_add_le {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a + b cb c - a

Alias of le_sub_iff_add_le'.

theorem sub_le_iff_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a - c b a b + c

@[simp]
theorem neg_le_sub_iff_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :
-b a - c c a + b

theorem neg_le_sub_iff_le_add' {α : Type u} [ordered_add_comm_group α] {a b c : α} :
-a b - c c a + b

theorem sub_le {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a - b c a - c b

theorem le_sub {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a b - c c b - a

theorem lt_sub_iff_add_lt' {α : Type u} [ordered_add_comm_group α] {a b c : α} :
b < c - a a + b < c

theorem add_lt_of_lt_sub_left {α : Type u} [ordered_add_comm_group α] {a b c : α} :
b < c - aa + b < c

Alias of lt_sub_iff_add_lt'.

theorem lt_sub_left_of_add_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a + b < cb < c - a

Alias of lt_sub_iff_add_lt'.

theorem lt_sub_iff_add_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a < c - b a + b < c

theorem add_lt_of_lt_sub_right {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a < c - ba + b < c

Alias of lt_sub_iff_add_lt.

theorem lt_sub_right_of_add_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a + b < ca < c - b

Alias of lt_sub_iff_add_lt.

theorem sub_lt_iff_lt_add' {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a - b < c a < b + c

theorem sub_left_lt_of_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a < b + ca - b < c

Alias of sub_lt_iff_lt_add'.

theorem lt_add_of_sub_left_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a - b < ca < b + c

Alias of sub_lt_iff_lt_add'.

theorem sub_lt_iff_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a - c < b a < b + c

theorem lt_add_of_sub_right_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a - c < ba < b + c

Alias of sub_lt_iff_lt_add.

theorem sub_right_lt_of_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a < b + ca - c < b

Alias of sub_lt_iff_lt_add.

@[simp]
theorem neg_lt_sub_iff_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :
-b < a - c c < a + b

theorem neg_lt_sub_iff_lt_add' {α : Type u} [ordered_add_comm_group α] {a b c : α} :
-a < b - c c < a + b

theorem sub_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a - b < c a - c < b

theorem lt_sub {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a < b - c c < b - a

Linearly ordered commutative groups

@[class]
structure linear_ordered_add_comm_group (α : Type u) :
Type u
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • neg : α → α
  • sub : α → α → α
  • sub_eq_add_neg : (∀ (a b : α), a - b = a + -b) . "try_refl_tac"
  • 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_1 : α), a bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • le_total : ∀ (a b : α), a b b a
  • decidable_le : decidable_rel has_le.le
  • decidable_eq : decidable_eq α
  • decidable_lt : decidable_rel has_lt.lt
  • add_le_add_left : ∀ (a b : α), a b∀ (c_1 : α), c_1 + a c_1 + b

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

Instances
@[class]
structure linear_ordered_comm_group (α : Type u) :
Type u
  • mul : α → α → α
  • mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • inv : α → α
  • div : α → α → α
  • div_eq_mul_inv : (∀ (a b : α), a / b = a * b⁻¹) . "try_refl_tac"
  • 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_1 : α), a bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • le_total : ∀ (a b : α), a b b a
  • decidable_le : decidable_rel has_le.le
  • decidable_eq : decidable_eq α
  • decidable_lt : decidable_rel has_lt.lt
  • mul_le_mul_left : ∀ (a b : α), a b∀ (c_1 : α), c_1 * a c_1 * b

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

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

theorem le_of_forall_pos_le_add {α : Type u} [linear_ordered_add_comm_group α] {a b : α} [densely_ordered α] (h : ∀ (ε : α), 0 < εa b + ε) :
a b

theorem min_neg_neg {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
min (-a) (-b) = -max a b

theorem max_neg_neg {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
max (-a) (-b) = -min a b

theorem min_sub_sub_right {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
min (a - c) (b - c) = min a b - c

theorem max_sub_sub_right {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
max (a - c) (b - c) = max a b - c

theorem min_sub_sub_left {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
min (a - b) (a - c) = a - max b c

theorem max_sub_sub_left {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
max (a - b) (a - c) = a - min b c

theorem max_zero_sub_eq_self {α : Type u} [linear_ordered_add_comm_group α] (a : α) :
max a 0 - max (-a) 0 = a

def abs {α : Type u} [linear_ordered_add_comm_group α] (a : α) :
α

abs a is the absolute value of a.

Equations
theorem abs_of_nonneg {α : Type u} [linear_ordered_add_comm_group α] {a : α} (h : 0 a) :
abs a = a

theorem abs_of_pos {α : Type u} [linear_ordered_add_comm_group α] {a : α} (h : 0 < a) :
abs a = a

theorem abs_of_nonpos {α : Type u} [linear_ordered_add_comm_group α] {a : α} (h : a 0) :
abs a = -a

theorem abs_of_neg {α : Type u} [linear_ordered_add_comm_group α] {a : α} (h : a < 0) :
abs a = -a

@[simp]
theorem abs_zero {α : Type u} [linear_ordered_add_comm_group α] :
abs 0 = 0

@[simp]
theorem abs_neg {α : Type u} [linear_ordered_add_comm_group α] (a : α) :
abs (-a) = abs a

@[simp]
theorem abs_pos {α : Type u} [linear_ordered_add_comm_group α] {a : α} :
0 < abs a a 0

theorem abs_pos_of_pos {α : Type u} [linear_ordered_add_comm_group α] {a : α} (h : 0 < a) :
0 < abs a

theorem abs_pos_of_neg {α : Type u} [linear_ordered_add_comm_group α] {a : α} (h : a < 0) :
0 < abs a

theorem abs_sub {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
abs (a - b) = abs (b - a)

theorem abs_le' {α : Type u} [linear_ordered_add_comm_group α] {a b : α} :
abs a b a b -a b

theorem abs_le {α : Type u} [linear_ordered_add_comm_group α] {a b : α} :
abs a b -b a a b

theorem le_abs_self {α : Type u} [linear_ordered_add_comm_group α] (a : α) :
a abs a

theorem neg_le_abs_self {α : Type u} [linear_ordered_add_comm_group α] (a : α) :
-a abs a

theorem abs_nonneg {α : Type u} [linear_ordered_add_comm_group α] (a : α) :
0 abs a

@[simp]
theorem abs_abs {α : Type u} [linear_ordered_add_comm_group α] (a : α) :
abs (abs a) = abs a

@[simp]
theorem abs_eq_zero {α : Type u} [linear_ordered_add_comm_group α] {a : α} :
abs a = 0 a = 0

@[simp]
theorem abs_nonpos_iff {α : Type u} [linear_ordered_add_comm_group α] {a : α} :
abs a 0 a = 0

theorem abs_lt {α : Type u} [linear_ordered_add_comm_group α] {a b : α} :
abs a < b -b < a a < b

theorem lt_abs {α : Type u} [linear_ordered_add_comm_group α] {a b : α} :
a < abs b a < b a < -b

theorem max_sub_min_eq_abs' {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
max a b - min a b = abs (a - b)

theorem max_sub_min_eq_abs {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
max a b - min a b = abs (b - a)

theorem abs_add {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
abs (a + b) abs a + abs b

theorem abs_sub_le_iff {α : Type u} [linear_ordered_add_comm_group α] {a b c : α} :
abs (a - b) c a - b c b - a c

theorem abs_sub_lt_iff {α : Type u} [linear_ordered_add_comm_group α] {a b c : α} :
abs (a - b) < c a - b < c b - a < c

theorem sub_le_of_abs_sub_le_left {α : Type u} [linear_ordered_add_comm_group α] {a b c : α} (h : abs (a - b) c) :
b - c a

theorem sub_le_of_abs_sub_le_right {α : Type u} [linear_ordered_add_comm_group α] {a b c : α} (h : abs (a - b) c) :
a - c b

theorem sub_lt_of_abs_sub_lt_left {α : Type u} [linear_ordered_add_comm_group α] {a b c : α} (h : abs (a - b) < c) :
b - c < a

theorem sub_lt_of_abs_sub_lt_right {α : Type u} [linear_ordered_add_comm_group α] {a b c : α} (h : abs (a - b) < c) :
a - c < b

theorem abs_sub_abs_le_abs_sub {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
abs a - abs b abs (a - b)

theorem abs_abs_sub_abs_le_abs_sub {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
abs (abs a - abs b) abs (a - b)

theorem abs_eq {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (hb : 0 b) :
abs a = b a = b a = -b

theorem abs_le_max_abs_abs {α : Type u} [linear_ordered_add_comm_group α] {a b c : α} (hab : a b) (hbc : b c) :
abs b max (abs a) (abs c)

theorem abs_le_abs {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h₀ : a b) (h₁ : -a b) :
abs a abs b

theorem abs_max_sub_max_le_abs {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
abs (max a c - max b c) abs (a - b)

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

theorem eq_of_abs_sub_eq_zero {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h : abs (a - b) = 0) :
a = b

theorem abs_by_cases {α : Type u} [linear_ordered_add_comm_group α] (P : α → Prop) {a : α} (h1 : P a) (h2 : P (-a)) :
P (abs a)

theorem abs_sub_le {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
abs (a - c) abs (a - b) + abs (b - c)

theorem abs_add_three {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
abs (a + b + c) abs a + abs b + abs c

theorem dist_bdd_within_interval {α : Type u} [linear_ordered_add_comm_group α] {a b lb ub : α} (hal : lb a) (hau : a ub) (hbl : lb b) (hbu : b ub) :
abs (a - b) ub - lb

theorem eq_of_abs_sub_nonpos {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h : abs (a - b) 0) :
a = b

theorem exists_zero_lt {α : Type u} [linear_ordered_add_comm_group α] [nontrivial α] :
∃ (a : α), 0 < a

@[class]
structure nonneg_add_comm_group (α : Type u_1) :
Type u_1

This is not so much a new structure as a construction mechanism for ordered groups, by specifying only the "positive cone" of the group.

Instances

A nonneg_add_comm_group is a linear_ordered_add_comm_group if nonneg is total and decidable.

Equations
@[instance]