mathlib documentation

algebra.order.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

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

Instances
@[instance]
def ordered_comm_group.to_comm_group (α : Type u) [self : ordered_comm_group α] :
@[class]
structure ordered_comm_group (α : Type u) :
Type u

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

Instances
@[instance]
@[protected, instance]
@[protected, instance]
def order_dual.has_neg {α : Type u} [h : has_neg α] :
Equations
@[protected, instance]
def order_dual.has_inv {α : Type u} [h : has_inv α] :
Equations
@[protected, instance]
def order_dual.has_sub {α : Type u} [h : has_sub α] :
Equations
@[protected, instance]
def order_dual.has_div {α : Type u} [h : has_div α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def order_dual.group {α : Type u} [h : group α] :
Equations
@[protected, instance]
def order_dual.add_group {α : Type u} [h : add_group α] :
Equations
@[protected, instance]
Equations
@[protected, instance]
def order_dual.comm_group {α : Type u} [h : comm_group α] :
Equations
@[simp]
theorem left.neg_nonpos_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a : α} :
-a 0 0 a
@[simp]
theorem left.inv_le_one_iff {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a : α} :
a⁻¹ 1 1 a

Uses left co(ntra)variant.

@[simp]
theorem left.nonneg_neg_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a : α} :
0 -a a 0
@[simp]
theorem left.one_le_inv_iff {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a : α} :
1 a⁻¹ a 1

Uses left co(ntra)variant.

@[simp]
theorem le_neg_add_iff_add_le {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
b -a + c a + b c
@[simp]
theorem le_inv_mul_iff_mul_le {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
b a⁻¹ * c a * b c
@[simp]
theorem inv_mul_le_iff_le_mul {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
b⁻¹ * a c a b * c
@[simp]
theorem neg_add_le_iff_le_add {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
-b + a c a b + c
theorem inv_le_iff_one_le_mul' {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b : α} :
a⁻¹ b 1 a * b
theorem neg_le_iff_add_nonneg' {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b : α} :
-a b 0 a + b
theorem le_inv_iff_mul_le_one_left {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b : α} :
a b⁻¹ b * a 1
theorem le_neg_iff_add_nonpos_left {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b : α} :
a -b b + a 0
theorem le_neg_add_iff_le {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b : α} :
0 -b + a b a
theorem le_inv_mul_iff_le {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b : α} :
1 b⁻¹ * a b a
theorem neg_add_nonpos_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b : α} :
-a + b 0 b a
theorem inv_mul_le_one_iff {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b : α} :
a⁻¹ * b 1 b a
@[simp]
theorem left.one_lt_inv_iff {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} :
1 < a⁻¹ a < 1

Uses left co(ntra)variant.

@[simp]
theorem left.neg_pos_iff {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
0 < -a a < 0
@[simp]
theorem left.neg_neg_iff {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
-a < 0 0 < a
@[simp]
theorem left.inv_lt_one_iff {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} :
a⁻¹ < 1 1 < a

Uses left co(ntra)variant.

@[simp]
theorem lt_inv_mul_iff_mul_lt {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
b < a⁻¹ * c a * b < c
@[simp]
theorem lt_neg_add_iff_add_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
b < -a + c a + b < c
@[simp]
theorem inv_mul_lt_iff_lt_mul {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
b⁻¹ * a < c a < b * c
@[simp]
theorem neg_add_lt_iff_lt_add {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
-b + a < c a < b + c
theorem inv_lt_iff_one_lt_mul' {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b : α} :
a⁻¹ < b 1 < a * b
theorem neg_lt_iff_pos_add' {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b : α} :
-a < b 0 < a + b
theorem lt_inv_iff_mul_lt_one' {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b : α} :
a < b⁻¹ b * a < 1
theorem lt_neg_iff_add_neg' {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b : α} :
a < -b b + a < 0
theorem lt_inv_mul_iff_lt {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b : α} :
1 < b⁻¹ * a b < a
theorem lt_neg_add_iff_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b : α} :
0 < -b + a b < a
theorem inv_mul_lt_one_iff {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b : α} :
a⁻¹ * b < 1 b < a
theorem neg_add_neg_iff {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b : α} :
-a + b < 0 b < a
@[simp]
theorem right.neg_nonpos_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a : α} :
-a 0 0 a
@[simp]
theorem right.inv_le_one_iff {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a : α} :
a⁻¹ 1 1 a

Uses right co(ntra)variant.

@[simp]
theorem right.nonneg_neg_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a : α} :
0 -a a 0
@[simp]
theorem right.one_le_inv_iff {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a : α} :
1 a⁻¹ a 1

Uses right co(ntra)variant.

theorem inv_le_iff_one_le_mul {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
a⁻¹ b 1 b * a
theorem neg_le_iff_add_nonneg {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
-a b 0 b + a
theorem le_neg_iff_add_nonpos_right {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
a -b a + b 0
theorem le_inv_iff_mul_le_one_right {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
a b⁻¹ a * b 1
@[simp]
theorem mul_inv_le_iff_le_mul {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} :
a * b⁻¹ c a c * b
@[simp]
theorem add_neg_le_iff_le_add {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} :
a + -b c a c + b
@[simp]
theorem le_mul_inv_iff_mul_le {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} :
c a * b⁻¹ c * b a
@[simp]
theorem le_add_neg_iff_add_le {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} :
c a + -b c + b a
@[simp]
theorem mul_inv_le_one_iff_le {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
a * b⁻¹ 1 a b
@[simp]
theorem add_neg_nonpos_iff_le {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
a + -b 0 a b
theorem le_add_neg_iff_le {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
0 a + -b b a
theorem le_mul_inv_iff_le {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
1 a * b⁻¹ b a
theorem mul_inv_le_one_iff {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
b * a⁻¹ 1 b a
theorem add_neg_nonpos_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
b + -a 0 b a
@[simp]
theorem right.neg_neg_iff {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a : α} :
-a < 0 0 < a
@[simp]
theorem right.inv_lt_one_iff {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a : α} :
a⁻¹ < 1 1 < a

Uses right co(ntra)variant.

@[simp]
theorem right.one_lt_inv_iff {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a : α} :
1 < a⁻¹ a < 1

Uses right co(ntra)variant.

@[simp]
theorem right.neg_pos_iff {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a : α} :
0 < -a a < 0
theorem neg_lt_iff_pos_add {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
-a < b 0 < b + a
theorem inv_lt_iff_one_lt_mul {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a⁻¹ < b 1 < b * a
theorem lt_inv_iff_mul_lt_one {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a < b⁻¹ a * b < 1
theorem lt_neg_iff_add_neg {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
a < -b a + b < 0
@[simp]
theorem mul_inv_lt_iff_lt_mul {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} :
a * b⁻¹ < c a < c * b
@[simp]
theorem add_neg_lt_iff_lt_add {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} :
a + -b < c a < c + b
@[simp]
theorem lt_add_neg_iff_add_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} :
c < a + -b c + b < a
@[simp]
theorem lt_mul_inv_iff_mul_lt {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} :
c < a * b⁻¹ c * b < a
@[simp]
theorem neg_add_neg_iff_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
a + -b < 0 a < b
@[simp]
theorem inv_mul_lt_one_iff_lt {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a * b⁻¹ < 1 a < b
theorem lt_mul_inv_iff_lt {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
1 < a * b⁻¹ b < a
theorem lt_add_neg_iff_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
0 < a + -b b < a
theorem add_neg_neg_iff {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
b + -a < 0 b < a
theorem mul_inv_lt_one_iff {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
b * a⁻¹ < 1 b < a
@[simp]
theorem neg_le_neg_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
-a -b b a
@[simp]
theorem inv_le_inv_iff {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
theorem le_of_neg_le_neg {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
-a -bb a

Alias of neg_le_neg_iff.

x ↦ x⁻¹ as an order-reversing equivalence.

Equations

x ↦ -x as an order-reversing equivalence.

Equations
theorem neg_le {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
-a b -b a
theorem inv_le' {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
theorem inv_le_of_inv_le' {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
a⁻¹ bb⁻¹ a

Alias of inv_le'.

theorem neg_le_of_neg_le {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
-a b-b a
theorem le_neg {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
a -b b -a
theorem le_inv' {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
theorem mul_inv_le_inv_mul_iff {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c d : α} :
a * b⁻¹ d⁻¹ * c d * a c * b
theorem add_neg_le_neg_add_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c d : α} :
a + -b -d + c d + a c + b
@[simp]
theorem sub_le_self_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (a : α) {b : α} :
a - b a 0 b
@[simp]
theorem div_le_self_iff {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a : α) {b : α} :
a / b a 1 b
@[simp]
theorem le_sub_self_iff {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (a : α) {b : α} :
a a - b b 0
@[simp]
theorem le_div_self_iff {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a : α) {b : α} :
a a / b b 1
theorem sub_le_self {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (a : α) {b : α} :
0 ba - b a

Alias of sub_le_self_iff.

@[simp]
theorem inv_lt_inv_iff {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a⁻¹ < b⁻¹ b < a
@[simp]
theorem neg_lt_neg_iff {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
-a < -b b < a
theorem neg_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
-a < b -b < a
theorem inv_lt' {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a⁻¹ < b b⁻¹ < a
theorem lt_inv' {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a < b⁻¹ b < a⁻¹
theorem lt_neg {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
a < -b b < -a
theorem lt_inv_of_lt_inv {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a < b⁻¹b < a⁻¹

Alias of lt_inv'.

theorem lt_neg_of_lt_neg {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
a < -bb < -a
theorem inv_lt_of_inv_lt' {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a⁻¹ < bb⁻¹ < a

Alias of inv_lt'.

theorem neg_lt_of_neg_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
-a < b-b < a
theorem mul_inv_lt_inv_mul_iff {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c d : α} :
a * b⁻¹ < d⁻¹ * c d * a < c * b
theorem add_neg_lt_neg_add_iff {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c d : α} :
a + -b < -d + c d + a < c + b
@[simp]
theorem div_lt_self_iff {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] (a : α) {b : α} :
a / b < a 1 < b
@[simp]
theorem sub_lt_self_iff {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] (a : α) {b : α} :
a - b < a 0 < b
theorem sub_lt_self {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] (a : α) {b : α} :
0 < ba - b < a

Alias of sub_lt_self_iff.

theorem left.neg_le_self {α : Type u} [add_group α] [preorder α] [covariant_class α α has_add.add has_le.le] {a : α} (h : 0 a) :
-a a
theorem left.inv_le_self {α : Type u} [group α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a : α} (h : 1 a) :
theorem neg_le_self {α : Type u} [add_group α] [preorder α] [covariant_class α α has_add.add has_le.le] {a : α} (h : 0 a) :
-a a

Alias of left.neg_le_self.

theorem left.self_le_neg {α : Type u} [add_group α] [preorder α] [covariant_class α α has_add.add has_le.le] {a : α} (h : a 0) :
a -a
theorem left.self_le_inv {α : Type u} [group α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a : α} (h : a 1) :
theorem left.inv_lt_self {α : Type u} [group α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} (h : 1 < a) :
a⁻¹ < a
theorem left.neg_lt_self {α : Type u} [add_group α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a : α} (h : 0 < a) :
-a < a
theorem neg_lt_self {α : Type u} [add_group α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a : α} (h : 0 < a) :
-a < a

Alias of left.neg_lt_self.

theorem left.self_lt_neg {α : Type u} [add_group α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a : α} (h : a < 0) :
a < -a
theorem left.self_lt_inv {α : Type u} [group α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} (h : a < 1) :
a < a⁻¹
theorem right.neg_le_self {α : Type u} [add_group α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a : α} (h : 0 a) :
-a a
theorem right.inv_le_self {α : Type u} [group α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a : α} (h : 1 a) :
theorem right.self_le_neg {α : Type u} [add_group α] [preorder α] [covariant_class α α (function.swap has_add.add) has_le.le] {a : α} (h : a 0) :
a -a
theorem right.self_le_inv {α : Type u} [group α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a : α} (h : a 1) :
theorem right.neg_lt_self {α : Type u} [add_group α] [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a : α} (h : 0 < a) :
-a < a
theorem right.inv_lt_self {α : Type u} [group α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a : α} (h : 1 < a) :
a⁻¹ < a
theorem right.self_lt_inv {α : Type u} [group α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a : α} (h : a < 1) :
a < a⁻¹
theorem right.self_lt_neg {α : Type u} [add_group α] [preorder α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a : α} (h : a < 0) :
a < -a
theorem inv_mul_le_iff_le_mul' {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
c⁻¹ * a b a b * c
theorem neg_add_le_iff_le_add' {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
-c + a b a b + c
@[simp]
theorem mul_inv_le_iff_le_mul' {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
a * b⁻¹ c a b * c
@[simp]
theorem add_neg_le_iff_le_add' {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
a + -b c a b + c
theorem add_neg_le_add_neg_iff {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c d : α} :
a + -b c + -d a + d c + b
theorem mul_inv_le_mul_inv_iff' {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c d : α} :
a * b⁻¹ c * d⁻¹ a * d c * b
theorem neg_add_lt_iff_lt_add' {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
-c + a < b a < b + c
theorem inv_mul_lt_iff_lt_mul' {α : Type u} [comm_group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
c⁻¹ * a < b a < b * c
@[simp]
theorem mul_inv_lt_iff_le_mul' {α : Type u} [comm_group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
a * b⁻¹ < c a < b * c
@[simp]
theorem add_neg_lt_iff_le_add' {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
a + -b < c a < b + c
theorem add_neg_lt_add_neg_iff {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c d : α} :
a + -b < c + -d a + d < c + b
theorem mul_inv_lt_mul_inv_iff' {α : Type u} [comm_group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c d : α} :
a * b⁻¹ < c * d⁻¹ a * d < c * b
theorem le_inv_of_le_inv {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
a b⁻¹b a⁻¹

Alias of le_inv'.

theorem le_neg_of_le_neg {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
a -bb -a
theorem one_le_of_inv_le_one {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a : α} :
a⁻¹ 11 a

Alias of left.inv_le_one_iff.

theorem nonneg_of_neg_nonpos {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a : α} :
-a 00 a
theorem le_one_of_one_le_inv {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a : α} :
1 a⁻¹a 1

Alias of left.one_le_inv_iff.

theorem nonpos_of_neg_nonneg {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a : α} :
0 -aa 0
theorem lt_of_inv_lt_inv {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a⁻¹ < b⁻¹b < a

Alias of inv_lt_inv_iff.

theorem lt_of_neg_lt_neg {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
-a < -bb < a
theorem one_lt_of_inv_lt_one {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} :
a⁻¹ < 11 < a

Alias of left.inv_lt_one_iff.

theorem pos_of_neg_neg {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
-a < 00 < a
theorem inv_lt_one_iff_one_lt {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} :
a⁻¹ < 1 1 < a

Alias of left.inv_lt_one_iff.

theorem neg_neg_iff_pos {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
-a < 0 0 < a
theorem inv_lt_one' {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} :
a⁻¹ < 1 1 < a

Alias of left.inv_lt_one_iff.

theorem neg_lt_zero {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
-a < 0 0 < a
theorem inv_of_one_lt_inv {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} :
1 < a⁻¹a < 1

Alias of left.one_lt_inv_iff.

theorem neg_of_neg_pos {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
0 < -aa < 0
theorem one_lt_inv_of_inv {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} :
a < 11 < a⁻¹

Alias of left.one_lt_inv_iff.

theorem neg_pos_of_neg {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
a < 00 < -a
theorem mul_le_of_le_inv_mul {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
b a⁻¹ * ca * b c

Alias of le_inv_mul_iff_mul_le.

theorem add_le_of_le_neg_add {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
b -a + ca + b c
theorem le_inv_mul_of_mul_le {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
a * b cb a⁻¹ * c

Alias of le_inv_mul_iff_mul_le.

theorem le_neg_add_of_add_le {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
a + b cb -a + c
theorem inv_mul_le_of_le_mul {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
a b * cb⁻¹ * a c

Alias of inv_mul_le_iff_le_mul.

theorem mul_lt_of_lt_inv_mul {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
b < a⁻¹ * ca * b < c

Alias of lt_inv_mul_iff_mul_lt.

theorem add_lt_of_lt_neg_add {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
b < -a + ca + b < c
theorem lt_inv_mul_of_mul_lt {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
a * b < cb < a⁻¹ * c

Alias of lt_inv_mul_iff_mul_lt.

theorem lt_neg_add_of_add_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
a + b < cb < -a + c
theorem inv_mul_lt_of_lt_mul {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
a < b * cb⁻¹ * a < c

Alias of inv_mul_lt_iff_lt_mul.

theorem lt_mul_of_inv_mul_lt {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
b⁻¹ * a < ca < b * c

Alias of inv_mul_lt_iff_lt_mul.

theorem lt_add_of_neg_add_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
-b + a < ca < b + c
theorem neg_add_lt_of_lt_add {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
a < b + c-b + a < c
theorem lt_mul_of_inv_mul_lt_left {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
b⁻¹ * a < ca < b * c

Alias of lt_mul_of_inv_mul_lt.

theorem lt_add_of_neg_add_lt_left {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
-b + a < ca < b + c
theorem inv_le_one' {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a : α} :
a⁻¹ 1 1 a

Alias of left.inv_le_one_iff.

theorem neg_nonpos {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a : α} :
-a 0 0 a
theorem one_le_inv' {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a : α} :
1 a⁻¹ a 1

Alias of left.one_le_inv_iff.

theorem neg_nonneg {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a : α} :
0 -a a 0
theorem one_lt_inv' {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} :
1 < a⁻¹ a < 1

Alias of left.one_lt_inv_iff.

theorem neg_pos {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
0 < -a a < 0
theorem ordered_comm_group.mul_lt_mul_left' {α : Type u_1} [has_mul α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {b c : α} (bc : b < c) (a : α) :
a * b < a * c

Alias of mul_lt_mul_left'.

theorem ordered_add_comm_group.add_lt_add_left {α : Type u_1} [has_add α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {b c : α} (bc : b < c) (a : α) :
a + b < a + c
theorem ordered_comm_group.le_of_mul_le_mul_left {α : Type u_1} [has_mul α] [has_le α] [contravariant_class α α has_mul.mul has_le.le] {a b c : α} (bc : a * b a * c) :
b c

Alias of le_of_mul_le_mul_left'.

theorem ordered_add_comm_group.le_of_add_le_add_left {α : Type u_1} [has_add α] [has_le α] [contravariant_class α α has_add.add has_le.le] {a b c : α} (bc : a + b a + c) :
b c
theorem ordered_comm_group.lt_of_mul_lt_mul_left {α : Type u_1} [has_mul α] [has_lt α] [contravariant_class α α has_mul.mul has_lt.lt] {a b c : α} (bc : a * b < a * c) :
b < c

Alias of lt_of_mul_lt_mul_left'.

theorem ordered_add_comm_group.lt_of_add_lt_add_left {α : Type u_1} [has_add α] [has_lt α] [contravariant_class α α has_add.add has_lt.lt] {a b c : α} (bc : a + b < a + c) :
b < c
def function.injective.ordered_add_comm_group {α : Type u} [ordered_add_comm_group α] {β : Type u_1} [has_zero β] [has_add β] [has_neg β] [has_sub β] (f : β → α) (hf : function.injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (inv : ∀ (x : β), f (-x) = -f x) (div : ∀ (x y : β), f (x - y) = f x - f y) :

Pullback an ordered_add_comm_group under an injective map.

Equations
def function.injective.ordered_comm_group {α : Type u} [ordered_comm_group α] {β : Type u_1} [has_one β] [has_mul β] [has_inv β] [has_div β] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (inv : ∀ (x : β), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : β), f (x / y) = f x / f y) :

Pullback an ordered_comm_group under an injective map. See note [reducible non-instances].

Equations
@[simp]
theorem div_le_div_iff_right {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (c : α) :
a / c b / c a b
@[simp]
theorem sub_le_sub_iff_right {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (c : α) :
a - c b - c a b
theorem sub_le_sub_right {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (h : a b) (c : α) :
a - c b - c
theorem div_le_div_right' {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (h : a b) (c : α) :
a / c b / c
@[simp]
theorem sub_nonneg {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
0 a - b b a
@[simp]
theorem one_le_div' {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
1 a / b b a
theorem le_of_sub_nonneg {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
0 a - bb a

Alias of sub_nonneg.

theorem sub_nonneg_of_le {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
b a0 a - b

Alias of sub_nonneg.

@[simp]
theorem div_le_one' {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} :
a / b 1 a b
@[simp]
theorem sub_nonpos {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
a - b 0 a b
theorem sub_nonpos_of_le {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
a ba - b 0

Alias of sub_nonpos.

theorem le_of_sub_nonpos {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
a - b 0a b

Alias of sub_nonpos.

theorem le_div_iff_mul_le {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} :
a c / b a * b c
theorem le_sub_iff_add_le {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} :
a c - b a + b c
theorem add_le_of_le_sub_right {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} :
a c - ba + b c

Alias of le_sub_iff_add_le.

theorem le_sub_right_of_add_le {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} :
a + b ca c - b

Alias of le_sub_iff_add_le.

theorem sub_le_iff_le_add {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b c : α} :
a - c b a b + c
theorem div_le_iff_le_mul {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b c : α} :
a / c b a b * c
@[simp]
theorem order_iso.add_right_apply {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] (a x : α) :
@[simp]
theorem order_iso.mul_right_apply {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a x : α) :
@[simp]
theorem order_iso.add_left_apply {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] (a x : α) :
@[simp]
theorem order_iso.mul_left_apply {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] (a x : α) :
@[simp]
theorem div_le_div_iff_left {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {b c : α} (a : α) :
a / b a / c c b
@[simp]
theorem sub_le_sub_iff_left {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {b c : α} (a : α) :
a - b a - c c b
theorem div_le_div_left' {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a b : α} (h : a b) (c : α) :
c / b c / a
theorem sub_le_sub_left {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} (h : a b) (c : α) :
c - b c - a
theorem sub_le_sub_iff {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c d : α} :
a - b c - d a + d c + b
theorem div_le_div_iff' {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c d : α} :
a / b c / d a * d c * b
theorem le_sub_iff_add_le' {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
b c - a a + b c
theorem le_div_iff_mul_le' {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
b c / a a * b c
theorem add_le_of_le_sub_left {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
b c - aa + b c

Alias of le_sub_iff_add_le'.

theorem le_sub_left_of_add_le {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
a + b cb c - a

Alias of le_sub_iff_add_le'.

theorem sub_le_iff_le_add' {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
a - b c a b + c
theorem div_le_iff_le_mul' {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
a / b c a b * c
theorem le_add_of_sub_left_le {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
a - b ca b + c

Alias of sub_le_iff_le_add'.

theorem sub_left_le_of_le_add {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
a b + ca - b c

Alias of sub_le_iff_le_add'.

@[simp]
theorem neg_le_sub_iff_le_add {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
-b a - c c a + b
@[simp]
theorem inv_le_div_iff_le_mul {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
b⁻¹ a / c c a * b
theorem inv_le_div_iff_le_mul' {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
a⁻¹ b / c c a * b
theorem neg_le_sub_iff_le_add' {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
-a b - c c a + b
theorem sub_le {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
a - b c a - c b
theorem div_le'' {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
a / b c a / c b
theorem le_sub {α : Type u} [add_comm_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a b c : α} :
a b - c c b - a
theorem le_div'' {α : Type u} [comm_group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] {a b c : α} :
a b / c c b / a
theorem div_le_div'' {α : Type u} [comm_group α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a b c d : α} (hab : a b) (hcd : c d) :
a / d b / c
theorem sub_le_sub {α : Type u} [add_comm_group α] [preorder α] [covariant_class α α has_add.add has_le.le] {a b c d : α} (hab : a b) (hcd : c d) :
a - d b - c
@[simp]
theorem sub_lt_sub_iff_right {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} (c : α) :
a - c < b - c a < b
@[simp]
theorem div_lt_div_iff_right {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} (c : α) :
a / c < b / c a < b
theorem div_lt_div_right' {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} (h : a < b) (c : α) :
a / c < b / c
theorem sub_lt_sub_right {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} (h : a < b) (c : α) :
a - c < b - c
@[simp]
theorem sub_pos {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
0 < a - b b < a
@[simp]
theorem one_lt_div' {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
1 < a / b b < a
theorem lt_of_sub_pos {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
0 < a - bb < a

Alias of sub_pos.

theorem sub_pos_of_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
b < a0 < a - b

Alias of sub_pos.

@[simp]
theorem div_lt_one' {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} :
a / b < 1 a < b
@[simp]
theorem sub_neg {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
a - b < 0 a < b
theorem lt_of_sub_neg {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
a - b < 0a < b

Alias of sub_neg.

theorem sub_neg_of_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
a < ba - b < 0

Alias of sub_neg.

theorem sub_lt_zero {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} :
a - b < 0 a < b

Alias of sub_neg.

theorem lt_sub_iff_add_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} :
a < c - b a + b < c
theorem lt_div_iff_mul_lt {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} :
a < c / b a * b < c
theorem add_lt_of_lt_sub_right {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} :
a < c - ba + b < c

Alias of lt_sub_iff_add_lt.

theorem lt_sub_right_of_add_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} :
a + b < ca < c - b

Alias of lt_sub_iff_add_lt.

theorem sub_lt_iff_lt_add {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} :
a - c < b a < b + c
theorem div_lt_iff_lt_mul {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} :
a / c < b a < b * c
theorem lt_add_of_sub_right_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} :
a - c < ba < b + c

Alias of sub_lt_iff_lt_add.

theorem sub_right_lt_of_lt_add {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} :
a < b + ca - c < b

Alias of sub_lt_iff_lt_add.

@[simp]
theorem div_lt_div_iff_left {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {b c : α} (a : α) :
a / b < a / c c < b
@[simp]
theorem sub_lt_sub_iff_left {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {b c : α} (a : α) :
a - b < a - c c < b
@[simp]
theorem neg_lt_sub_iff_lt_add {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b c : α} :
-a < b - c c < a + b
@[simp]
theorem inv_lt_div_iff_lt_mul {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b c : α} :
a⁻¹ < b / c c < a * b
theorem sub_lt_sub_left {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] [covariant_class α α (function.swap has_add.add) has_lt.lt] {a b : α} (h : a < b) (c : α) :
c - b < c - a
theorem div_lt_div_left' {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] {a b : α} (h : a < b) (c : α) :
c / b < c / a
theorem div_lt_div_iff' {α : Type u} [comm_group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c d : α} :
a / b < c / d a * d < c * b
theorem sub_lt_sub_iff {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c d : α} :
a - b < c - d a + d < c + b
theorem lt_div_iff_mul_lt' {α : Type u} [comm_group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
b < c / a a * b < c
theorem lt_sub_iff_add_lt' {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
b < c - a a + b < c
theorem add_lt_of_lt_sub_left {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
b < c - aa + b < c

Alias of lt_sub_iff_add_lt'.

theorem lt_sub_left_of_add_lt {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
a + b < cb < c - a

Alias of lt_sub_iff_add_lt'.

theorem div_lt_iff_lt_mul' {α : Type u} [comm_group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
a / b < c a < b * c
theorem sub_lt_iff_lt_add' {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
a - b < c a < b + c
theorem sub_left_lt_of_lt_add {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
a < b + ca - b < c

Alias of sub_lt_iff_lt_add'.

theorem lt_add_of_sub_left_lt {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
a - b < ca < b + c

Alias of sub_lt_iff_lt_add'.

theorem inv_lt_div_iff_lt_mul' {α : Type u} [comm_group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
b⁻¹ < a / c c < a * b
theorem neg_lt_sub_iff_lt_add' {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
-b < a - c c < a + b
theorem sub_lt {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
a - b < c a - c < b
theorem div_lt'' {α : Type u} [comm_group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
a / b < c a / c < b
theorem lt_div'' {α : Type u} [comm_group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] {a b c : α} :
a < b / c c < b / a
theorem lt_sub {α : Type u} [add_comm_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a b c : α} :
a < b - c c < b - a
theorem div_lt_div'' {α : Type u} [comm_group α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a b c d : α} (hab : a < b) (hcd : c < d) :
a / d < b / c
theorem sub_lt_sub {α : Type u} [add_comm_group α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a b c d : α} (hab : a < b) (hcd : c < d) :
a - d < b - c
theorem le_of_forall_one_lt_lt_mul {α : Type u} [group α] [linear_order α] [covariant_class α α has_mul.mul has_le.le] {a b : α} (h : ∀ (ε : α), 1 < εa < b * ε) :
a b
theorem le_of_forall_pos_lt_add {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a b : α} (h : ∀ (ε : α), 0 < εa < b + ε) :
a b
theorem le_iff_forall_pos_lt_add {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a b : α} :
a b ∀ (ε : α), 0 < εa < b + ε
theorem le_iff_forall_one_lt_lt_mul {α : Type u} [group α] [linear_order α] [covariant_class α α has_mul.mul has_le.le] {a b : α} :
a b ∀ (ε : α), 1 < εa < b * ε
@[simp]
theorem sub_le_sub_flip {α : Type u_1} [add_comm_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a b : α} :
a - b b - a a b
@[simp]
theorem div_le_div_flip {α : Type u_1} [comm_group α] [linear_order α] [covariant_class α α has_mul.mul has_le.le] {a b : α} :
a / b b / a a b
@[simp]
theorem max_zero_sub_max_neg_zero_eq_self {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] (a : α) :
max a 0 - max (-a) 0 = a
@[simp]
theorem max_one_div_max_inv_one_eq_self {α : Type u} [group α] [linear_order α] [covariant_class α α has_mul.mul has_le.le] (a : α) :
max a 1 / max a⁻¹ 1 = a
theorem max_zero_sub_eq_self {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] (a : α) :
max a 0 - max (-a) 0 = a

Alias of max_zero_sub_max_neg_zero_eq_self.

theorem le_of_forall_one_lt_le_mul {α : Type u} [group α] [linear_order α] [covariant_class α α has_mul.mul has_le.le] [densely_ordered α] {a b : α} (h : ∀ (ε : α), 1 < εa b * ε) :
a b
theorem le_of_forall_pos_le_add {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] [densely_ordered α] {a b : α} (h : ∀ (ε : α), 0 < εa b + ε) :
a b
theorem le_of_forall_lt_one_mul_le {α : Type u} [group α] [linear_order α] [covariant_class α α has_mul.mul has_le.le] [densely_ordered α] {a b : α} (h : ∀ (ε : α), ε < 1a * ε b) :
a b
theorem le_of_forall_neg_add_le {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] [densely_ordered α] {a b : α} (h : ∀ (ε : α), ε < 0a + ε b) :
a b
theorem le_of_forall_one_lt_div_le {α : Type u} [group α] [linear_order α] [covariant_class α α has_mul.mul has_le.le] [densely_ordered α] {a b : α} (h : ∀ (ε : α), 1 < εa / ε b) :
a b
theorem le_of_forall_pos_sub_le {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] [densely_ordered α] {a b : α} (h : ∀ (ε : α), 0 < εa - ε b) :
a b
theorem le_iff_forall_pos_le_add {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] [densely_ordered α] {a b : α} :
a b ∀ (ε : α), 0 < εa b + ε
theorem le_iff_forall_one_lt_le_mul {α : Type u} [group α] [linear_order α] [covariant_class α α has_mul.mul has_le.le] [densely_ordered α] {a b : α} :
a b ∀ (ε : α), 1 < εa b * ε
theorem le_iff_forall_neg_add_le {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] [densely_ordered α] {a b : α} :
a b ∀ (ε : α), ε < 0a + ε b
theorem le_iff_forall_lt_one_mul_le {α : Type u} [group α] [linear_order α] [covariant_class α α has_mul.mul has_le.le] [densely_ordered α] {a b : α} :
a b ∀ (ε : α), ε < 1a * ε b

Linearly ordered commutative groups #

@[class]
structure linear_ordered_add_comm_group (α : Type u) :
Type u

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_add_comm_group_with_top (α : Type u_1) :
Type u_1

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

Instances
@[class]
structure linear_ordered_comm_group (α : Type u) :
Type u

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

Instances
def function.injective.linear_ordered_comm_group {α : Type u} [linear_ordered_comm_group α] {β : Type u_1} [has_one β] [has_mul β] [has_inv β] [has_div β] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) (inv : ∀ (x : β), f x⁻¹ = (f x)⁻¹) (div : ∀ (x y : β), f (x / y) = f x / f y) :

Pullback a linear_ordered_comm_group under an injective map. See note [reducible non-instances].

Equations
def function.injective.linear_ordered_add_comm_group {α : Type u} [linear_ordered_add_comm_group α] {β : Type u_1} [has_zero β] [has_add β] [has_neg β] [has_sub β] (f : β → α) (hf : function.injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) (inv : ∀ (x : β), f (-x) = -f x) (div : ∀ (x y : β), f (x - y) = f x - f y) :

Pullback a linear_ordered_add_comm_group under an injective map.

Equations
theorem linear_ordered_comm_group.mul_lt_mul_left' {α : Type u} [linear_ordered_comm_group α] (a b : α) (h : a < b) (c : α) :
c * a < c * b
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 min_neg_neg {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
min (-a) (-b) = -max a b
theorem min_inv_inv' {α : Type u} [linear_ordered_comm_group α] (a b : α) :
theorem max_inv_inv' {α : Type u} [linear_ordered_comm_group α] (a b : α) :
theorem max_neg_neg {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
max (-a) (-b) = -min a b
theorem min_div_div_right' {α : Type u} [linear_ordered_comm_group α] (a b c : α) :
min (a / c) (b / c) = min a b / c
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_div_div_right' {α : Type u} [linear_ordered_comm_group α] (a b c : α) :
max (a / c) (b / c) = max 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_div_div_left' {α : Type u} [linear_ordered_comm_group α] (a b c : α) :
min (a / b) (a / c) = a / max 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_div_div_left' {α : Type u} [linear_ordered_comm_group α] (a b c : α) :
max (a / b) (a / c) = a / min 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 eq_zero_of_neg_eq {α : Type u} [linear_ordered_add_comm_group α] {a : α} (h : -a = a) :
a = 0
theorem eq_one_of_inv_eq' {α : Type u} [linear_ordered_comm_group α] {a : α} (h : a⁻¹ = a) :
a = 1
theorem exists_one_lt' {α : Type u} [linear_ordered_comm_group α] [nontrivial α] :
∃ (a : α), 1 < a
theorem exists_zero_lt {α : Type u} [linear_ordered_add_comm_group α] [nontrivial α] :
∃ (a : α), 0 < a
@[protected, instance]
@[protected, instance]
@[protected, instance]
def has_neg_lattice_has_abs {α : Type u} [has_neg α] [lattice α] :
Equations
@[protected, instance]
def has_inv_lattice_has_abs {α : Type u} [has_inv α] [lattice α] :

abs a is the absolute value of a.

Equations
theorem abs_eq_sup_inv {α : Type u} [has_inv α] [lattice α] (a : α) :
theorem abs_eq_sup_neg {α : Type u} [has_neg α] [lattice α] (a : α) :
|a| = a -a
theorem abs_eq_max_neg {α : Type u} [has_neg α] [linear_order α] {a : α} :
|a| = max a (-a)
theorem abs_choice {α : Type u} [has_neg α] [linear_order α] (x : α) :
|x| = x |x| = -x
theorem abs_le' {α : Type u} [has_neg α] [linear_order α] {a b : α} :
|a| b a b -a b
theorem le_abs {α : Type u} [has_neg α] [linear_order α] {a b : α} :
a |b| a b a -b
theorem le_abs_self {α : Type u} [has_neg α] [linear_order α] (a : α) :
a |a|
theorem neg_le_abs_self {α : Type u} [has_neg α] [linear_order α] (a : α) :
-a |a|
theorem lt_abs {α : Type u} [has_neg α] [linear_order α] {a b : α} :
a < |b| a < b a < -b
theorem abs_le_abs {α : Type u} [has_neg α] [linear_order α] {a b : α} (h₀ : a b) (h₁ : -a b) :
theorem abs_by_cases {α : Type u} [has_neg α] [linear_order α] (P : α → Prop) {a : α} (h1 : P a) (h2 : P (-a)) :
P |a|
@[simp]
theorem abs_neg {α : Type u} [add_group α] [linear_order α] (a : α) :
|-a| = |a|
theorem eq_or_eq_neg_of_abs_eq {α : Type u} [add_group α] [linear_order α] {a b : α} (h : |a| = b) :
a = b a = -b
theorem abs_eq_abs {α : Type u} [add_group α] [linear_order α] {a b : α} :
|a| = |b| a = b a = -b
theorem abs_sub_comm {α : Type u} [add_group α] [linear_order α] (a b : α) :
|a - b| = |b - a|
theorem abs_of_nonneg {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} (h : 0 a) :
|a| = a
theorem abs_of_pos {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} (h : 0 < a) :
|a| = a
theorem abs_of_nonpos {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} (h : a 0) :
|a| = -a
theorem abs_of_neg {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} (h : a < 0) :
|a| = -a
@[simp]
theorem abs_zero {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] :
|0| = 0
@[simp]
theorem abs_pos {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} :
0 < |a| a 0
theorem abs_pos_of_pos {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} (h : 0 < a) :
0 < |a|
theorem abs_pos_of_neg {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} (h : a < 0) :
0 < |a|
theorem neg_abs_le_self {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] (a : α) :
-|a| a
theorem abs_nonneg {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] (a : α) :
0 |a|
@[simp]
theorem abs_abs {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] (a : α) :
@[simp]
theorem abs_eq_zero {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} :
|a| = 0 a = 0
@[simp]
theorem abs_nonpos_iff {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} :
|a| 0 a = 0
theorem abs_lt {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a b : α} [covariant_class α α (function.swap has_add.add) has_le.le] :
|a| < b -b < a a < b
theorem neg_lt_of_abs_lt {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a b : α} [covariant_class α α (function.swap has_add.add) has_le.le] (h : |a| < b) :
-b < a
theorem lt_of_abs_lt {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a b : α} [covariant_class α α (function.swap has_add.add) has_le.le] (h : |a| < b) :
a < b
theorem max_sub_min_eq_abs {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (a b : α) :
max a b - min a b = |b - a|
theorem abs_le {α : Type u} [linear_ordered_add_comm_group α] {a b : α} :
|a| b -b a a b
theorem le_abs' {α : Type u} [linear_ordered_add_comm_group α] {a b : α} :
a |b| b -a a b
theorem neg_le_of_abs_le {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h : |a| b) :
-b a
theorem le_of_abs_le {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h : |a| b) :
a b
theorem abs_add {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
|a + b| |a| + |b|

The triangle inequality in linear_ordered_add_comm_groups.

theorem abs_sub {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
|a - b| |a| + |b|
theorem abs_sub_le_iff {α : Type u} [linear_ordered_add_comm_group α] {a b c : α} :
|a - b| c a - b c b - a c
theorem abs_sub_lt_iff {α : Type u} [linear_ordered_add_comm_group α] {a b c : α} :
|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 : |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 : |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 : |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 : |a - b| < c) :
a - c < b
theorem abs_sub_abs_le_abs_sub {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
|a| - |b| |a - b|
theorem abs_abs_sub_abs_le_abs_sub {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
||a| - |b|| |a - b|
theorem abs_eq {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (hb : 0 b) :
|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) :
theorem eq_of_abs_sub_eq_zero {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h : |a - b| = 0) :
a = b
theorem abs_sub_le {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
|a - c| |a - b| + |b - c|
theorem abs_add_three {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
|a + b + c| |a| + |b| + |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) :
|a - b| ub - lb
theorem eq_of_abs_sub_nonpos {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h : |a - b| 0) :
a = b
theorem max_sub_max_le_max {α : Type u} [linear_ordered_add_comm_group α] (a b c d : α) :
max a b - max c d max (a - c) (b - d)
theorem abs_max_sub_max_le_max {α : Type u} [linear_ordered_add_comm_group α] (a b c d : α) :
|max a b - max c d| max |a - c| |b - d|
theorem abs_min_sub_min_le_max {α : Type u} [linear_ordered_add_comm_group α] (a b c d : α) :
|min a b - min c d| max |a - c| |b - d|
theorem abs_max_sub_max_le_abs {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
|max a c - max b c| |a - b|
@[protected, instance]
Equations
@[nolint]
structure add_comm_group.positive_cone (α : Type u_1) [add_comm_group α] :
Type u_1
  • nonneg : α → Prop
  • pos : α → Prop
  • pos_iff : (∀ (a : α), self.pos a self.nonneg a ¬self.nonneg (-a)) . "order_laws_tac"
  • zero_nonneg : self.nonneg 0
  • add_nonneg : ∀ {a b : α}, self.nonneg aself.nonneg bself.nonneg (a + b)
  • nonneg_antisymm : ∀ {a : α}, self.nonneg aself.nonneg (-a)a = 0

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

Forget that a total_positive_cone is total.

@[nolint]
structure add_comm_group.total_positive_cone (α : Type u_1) [add_comm_group α] :
Type u_1

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

Construct an ordered_add_comm_group by designating a positive cone in an existing add_comm_group.

Equations

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

Equations
theorem neg_le_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :
a b-b -a
theorem inv_le_inv' {α : Type u} [ordered_comm_group α] {a b : α} :
a bb⁻¹ a⁻¹
theorem neg_lt_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :
a < b-b < -a
theorem inv_lt_inv' {α : Type u} [ordered_comm_group α] {a b : α} :
a < bb⁻¹ < a⁻¹
theorem inv_lt_one_of_one_lt {α : Type u} [ordered_comm_group α] {a : α} :
1 < aa⁻¹ < 1
theorem neg_neg_of_pos {α : Type u} [ordered_add_comm_group α] {a : α} :
0 < a-a < 0
theorem inv_le_one_of_one_le {α : Type u} [ordered_comm_group α] {a : α} :
1 aa⁻¹ 1
theorem neg_nonpos_of_nonneg {α : Type u} [ordered_add_comm_group α] {a : α} :
0 a-a 0
theorem one_le_inv_of_le_one {α : Type u} [ordered_comm_group α] {a : α} :
a 11 a⁻¹
theorem neg_nonneg_of_nonpos {α : Type u} [ordered_add_comm_group α] {a : α} :
a 00 -a