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.

source
@[protected, instance]
def group.covariant_class_le.to_contravariant_class_le {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] :
contravariant_class α α has_mul.mul has_le.le
source
@[protected, instance]
def add_group.covariant_class_le.to_contravariant_class_le {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] :
contravariant_class α α has_add.add has_le.le
source
@[protected, instance]
def add_group.swap.covariant_class_le.to_contravariant_class_le {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] :
contravariant_class α α (function.swap has_add.add) has_le.le
source
@[protected, instance]
def group.swap.covariant_class_le.to_contravariant_class_le {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] :
contravariant_class α α (function.swap has_mul.mul) has_le.le
source
@[protected, instance]
def group.covariant_class_lt.to_contravariant_class_lt {α : Type u} [group α] [has_lt α] [covariant_class α α has_mul.mul has_lt.lt] :
contravariant_class α α has_mul.mul has_lt.lt
source
@[protected, instance]
def add_group.covariant_class_lt.to_contravariant_class_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] :
contravariant_class α α has_add.add has_lt.lt
source
@[protected, instance]
def add_group.swap.covariant_class_lt.to_contravariant_class_lt {α : Type u} [add_group α] [has_lt α] [covariant_class α α (function.swap has_add.add) has_lt.lt] :
contravariant_class α α (function.swap has_add.add) has_lt.lt
source
@[protected, instance]
def group.swap.covariant_class_lt.to_contravariant_class_lt {α : Type u} [group α] [has_lt α] [covariant_class α α (function.swap has_mul.mul) has_lt.lt] :
contravariant_class α α (function.swap has_mul.mul) has_lt.lt
source
@[instance]
def ordered_add_comm_group.to_partial_order (α : Type u) [self : ordered_add_comm_group α] :
partial_order α
source
@[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
source
@[instance]
def ordered_add_comm_group.to_add_comm_group (α : Type u) [self : ordered_add_comm_group α] :
add_comm_group α
source
@[instance]
def ordered_comm_group.to_comm_group (α : Type u) [self : ordered_comm_group α] :
comm_group α
source
@[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
source
@[instance]
def ordered_comm_group.to_partial_order (α : Type u) [self : ordered_comm_group α] :
partial_order α
source
@[protected, instance]
def ordered_add_comm_group.to_covariant_class_left_le (α : Type u) [ordered_add_comm_group α] :
covariant_class α α has_add.add has_le.le
source
@[protected, instance]
def ordered_comm_group.to_covariant_class_left_le (α : Type u) [ordered_comm_group α] :
covariant_class α α has_mul.mul has_le.le
source
@[protected, instance]
def add_units.ordered_add_comm_group {α : Type u} [ordered_add_comm_monoid α] :
ordered_add_comm_group (add_units α)

The units of an ordered commutative additive monoid form an ordered commutative additive group.

Equations
source
@[protected, instance]
def units.ordered_comm_group {α : Type u} [ordered_comm_monoid α] :
ordered_comm_group αˣ

The units of an ordered commutative monoid form an ordered commutative group.

Equations
source
@[protected, instance]
def ordered_add_comm_group.to_ordered_cancel_add_comm_monoid (α : Type u) [s : ordered_add_comm_group α] :
ordered_cancel_add_comm_monoid α
Equations
source
@[protected, instance]
def ordered_comm_group.to_ordered_cancel_comm_monoid (α : Type u) [s : ordered_comm_group α] :
ordered_cancel_comm_monoid α
Equations
source
@[protected, instance]
def ordered_add_comm_group.has_exists_add_of_le (α : Type u) [ordered_add_comm_group α] :
has_exists_add_of_le α
source
@[protected, instance]
def ordered_comm_group.has_exists_mul_of_le (α : Type u) [ordered_comm_group α] :
has_exists_mul_of_le α
source
@[protected, instance]
def order_dual.has_neg {α : Type u} [h : has_neg α] :
has_neg (order_dual α)
Equations
source
@[protected, instance]
def order_dual.has_inv {α : Type u} [h : has_inv α] :
has_inv (order_dual α)
Equations
source
@[protected, instance]
def order_dual.has_sub {α : Type u} [h : has_sub α] :
has_sub (order_dual α)
Equations
source
@[protected, instance]
def order_dual.has_div {α : Type u} [h : has_div α] :
has_div (order_dual α)
Equations
source
@[protected, instance]
def order_dual.has_involutive_neg {α : Type u} [h : has_involutive_neg α] :
has_involutive_neg (order_dual α)
Equations
source
@[protected, instance]
def order_dual.has_involutive_inv {α : Type u} [h : has_involutive_inv α] :
has_involutive_inv (order_dual α)
Equations
source
@[protected, instance]
def order_dual.div_inv_monoid {α : Type u} [h : div_inv_monoid α] :
div_inv_monoid (order_dual α)
Equations
source
@[protected, instance]
def order_dual.sub_neg_add_monoid {α : Type u} [h : sub_neg_monoid α] :
sub_neg_monoid (order_dual α)
Equations
source
@[protected, instance]
def order_dual.group {α : Type u} [h : group α] :
group (order_dual α)
Equations
source
@[protected, instance]
def order_dual.add_group {α : Type u} [h : add_group α] :
add_group (order_dual α)
Equations
source
@[protected, instance]
def order_dual.add_comm_group {α : Type u} [h : add_comm_group α] :
add_comm_group (order_dual α)
Equations
source
@[protected, instance]
def order_dual.comm_group {α : Type u} [h : comm_group α] :
comm_group (order_dual α)
Equations
source
@[protected, instance]
def order_dual.ordered_add_comm_group {α : Type u} [ordered_add_comm_group α] :
ordered_add_comm_group (order_dual α)
Equations
source
@[protected, instance]
def order_dual.ordered_comm_group {α : Type u} [ordered_comm_group α] :
ordered_comm_group (order_dual α)
Equations
source
@[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
source
@[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.

source
@[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
source
@[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.

source
@[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
source
@[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
source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
@[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.

source
@[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
source
@[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
source
@[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.

source
@[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
source
@[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
source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
@[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
source
@[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.

source
@[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
source
@[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.

source
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
source
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
source
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
source
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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
@[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

Uses right co(ntra)variant.

source
@[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.

source
@[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.

source
@[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

Uses right co(ntra)variant.

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

Alias of neg_le_neg_iff.

source
@[simp]
theorem order_iso.neg_apply (α : Type u) [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (ᾰ : α) :
⇑(order_iso.neg α) ᾰ = ⇑order_dual.to_dual (-ᾰ)
source
@[simp]
theorem order_iso.neg_symm_apply (α : Type u) [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] [covariant_class α α (function.swap has_add.add) has_le.le] (ᾰ : order_dual α) :
⇑(rel_iso.symm (order_iso.neg α)) ᾰ = -⇑order_dual.of_dual ᾰ
source
def order_iso.inv (α : Type u) [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] :
α ≃o order_dual α

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

Equations
source
@[simp]
theorem order_iso.inv_apply (α : Type u) [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ᾰ : α) :
⇑(order_iso.inv α) ᾰ = ⇑order_dual.to_dual ᾰ⁻¹
source
def order_iso.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] :
α ≃o order_dual α

x ↦ -x as an order-reversing equivalence.

Equations
source
@[simp]
theorem order_iso.inv_symm_apply (α : Type u) [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] [covariant_class α α (function.swap has_mul.mul) has_le.le] (ᾰ : order_dual α) :
⇑(rel_iso.symm (order_iso.inv α)) ᾰ = (⇑order_dual.of_dual ᾰ)⁻¹
source
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
source
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 : α} :
a⁻¹ ≤ b ↔ b⁻¹ ≤ a
source
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⁻¹ ≤ b → b⁻¹ ≤ a

Alias of inv_le'.

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

Alias of sub_le_self_iff.

source
@[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
source
@[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
source
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
source
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
source
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⁻¹
source
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
source
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'.

source
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 < -b → b < -a
source
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⁻¹ < b → b⁻¹ < a

Alias of inv_lt'.

source
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
source
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
source
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
source
@[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
source
@[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
source
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 < b → a - b < a

Alias of sub_lt_self_iff.

source
theorem left.neg_le_self {α : Type u} [add_group α] [preorder α] [covariant_class α α has_add.add has_le.le] {a : α} (h : 0 ≤ a) :
-a ≤ a
source
theorem left.inv_le_self {α : Type u} [group α] [preorder α] [covariant_class α α has_mul.mul has_le.le] {a : α} (h : 1 ≤ a) :
a⁻¹ ≤ a
source
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.

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

source
theorem left.self_lt_neg {α : Type u} [add_group α] [preorder α] [covariant_class α α has_add.add has_lt.lt] {a : α} (h : a < 0) :
a < -a
source
theorem left.self_lt_inv {α : Type u} [group α] [preorder α] [covariant_class α α has_mul.mul has_lt.lt] {a : α} (h : a < 1) :
a < a⁻¹
source
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
source
theorem right.inv_le_self {α : Type u} [group α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a : α} (h : 1 ≤ a) :
a⁻¹ ≤ a
source
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
source
theorem right.self_le_inv {α : Type u} [group α] [preorder α] [covariant_class α α (function.swap has_mul.mul) has_le.le] {a : α} (h : a ≤ 1) :
a ≤ a⁻¹
source
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
source
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
source
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⁻¹
source
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
source
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
source
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
source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
@[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
source
@[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
source
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
source
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
source
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'.

source
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 ≤ -b → b ≤ -a
source
theorem one_le_of_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.

source
theorem nonneg_of_neg_nonpos {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a : α} :
-a ≤ 0 → 0 ≤ a
source
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.

source
theorem nonpos_of_neg_nonneg {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a : α} :
0 ≤ -a → a ≤ 0
source
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.

source
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 < -b → b < a
source
theorem one_lt_of_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.

source
theorem pos_of_neg_neg {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
-a < 0 → 0 < a
source
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.

source
theorem neg_neg_iff_pos {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
-a < 0 ↔ 0 < a

Alias of left.neg_neg_iff.

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

source
theorem neg_lt_zero {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
-a < 0 ↔ 0 < a

Alias of left.neg_neg_iff.

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

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

Alias of left.one_lt_inv_iff.

source
theorem neg_pos_of_neg {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
a < 0 → 0 < -a
source
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⁻¹ * c → a * b ≤ c

Alias of le_inv_mul_iff_mul_le.

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

Alias of le_inv_mul_iff_mul_le.

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

Alias of inv_mul_le_iff_le_mul.

source
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⁻¹ * c → a * b < c

Alias of lt_inv_mul_iff_mul_lt.

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

Alias of lt_inv_mul_iff_mul_lt.

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

Alias of inv_mul_lt_iff_lt_mul.

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

Alias of inv_mul_lt_iff_lt_mul.

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

Alias of lt_mul_of_inv_mul_lt.

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

Alias of lt_add_of_neg_add_lt.

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

source
theorem neg_nonpos {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a : α} :
-a ≤ 0 ↔ 0 ≤ a

Alias of left.neg_nonpos_iff.

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

source
theorem neg_nonneg {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] {a : α} :
0 ≤ -a ↔ a ≤ 0

Alias of left.nonneg_neg_iff.

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

source
theorem neg_pos {α : Type u} [add_group α] [has_lt α] [covariant_class α α has_add.add has_lt.lt] {a : α} :
0 < -a ↔ a < 0

Alias of left.neg_pos_iff.

source
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'.

source
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

Alias of add_lt_add_left.

source
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'.

source
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

Alias of le_of_add_le_add_left.

source
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'.

source
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

Alias of lt_of_add_lt_add_left.

source
def function.injective.ordered_add_comm_group {α : Type u} [ordered_add_comm_group α] {β : Type u_1} [has_zero β] [has_add β] [has_neg β] [has_sub β] [has_scalar ℕ β] [has_scalar ℤ β] (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) (npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : β) (n : ℤ), f (n • x) = n • f x) :
ordered_add_comm_group β

Pullback an ordered_add_comm_group under an injective map.

Equations
source
def function.injective.ordered_comm_group {α : Type u} [ordered_comm_group α] {β : Type u_1} [has_one β] [has_mul β] [has_inv β] [has_div β] [has_pow β ℕ] [has_pow β ℤ] (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) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : β) (n : ℤ), f (x ^ n) = f x ^ n) :
ordered_comm_group β

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

Equations
source
@[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
source
@[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
source
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
source
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
source
@[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
source
@[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
source
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 - b → b ≤ a

Alias of sub_nonneg.

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

Alias of sub_nonneg.

source
@[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
source
@[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
source
theorem sub_nonpos_of_le {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] {a b : α} :
a ≤ b → a - b ≤ 0

Alias of sub_nonpos.

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

Alias of sub_nonpos.

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

Alias of le_sub_iff_add_le.

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

Alias of le_sub_iff_add_le.

source
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
source
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
source
@[protected, instance]
def add_group.to_has_ordered_sub {α : Type u_1} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] :
has_ordered_sub α
Equations
source
@[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 : α) :
⇑(order_iso.add_right a) x = x + a
source
@[simp]
theorem order_iso.mul_right_apply {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a x : α) :
⇑(order_iso.mul_right a) x = x * a
source
@[simp]
theorem order_iso.mul_right_to_equiv {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a : α) :
(order_iso.mul_right a).to_equiv = equiv.mul_right a
source
def order_iso.add_right {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] (a : α) :
α ≃o α

equiv.add_right as an order_iso. See also order_embedding.add_right.

Equations
source
def order_iso.mul_right {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a : α) :
α ≃o α

equiv.mul_right as an order_iso. See also order_embedding.mul_right.

Equations
source
@[simp]
theorem order_iso.add_right_to_equiv {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] (a : α) :
(order_iso.add_right a).to_equiv = equiv.add_right a
source
@[simp]
theorem order_iso.add_right_symm {α : Type u} [add_group α] [has_le α] [covariant_class α α (function.swap has_add.add) has_le.le] (a : α) :
(order_iso.add_right a).symm = order_iso.add_right (-a)
source
@[simp]
theorem order_iso.mul_right_symm {α : Type u} [group α] [has_le α] [covariant_class α α (function.swap has_mul.mul) has_le.le] (a : α) :
(order_iso.mul_right a).symm = order_iso.mul_right a⁻¹
source
@[simp]
theorem order_iso.mul_left_to_equiv {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] (a : α) :
(order_iso.mul_left a).to_equiv = equiv.mul_left a
source
@[simp]
theorem order_iso.add_left_to_equiv {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] (a : α) :
(order_iso.add_left a).to_equiv = equiv.add_left a
source
@[simp]
theorem order_iso.add_left_apply {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] (a x : α) :
⇑(order_iso.add_left a) x = a + x
source
def order_iso.add_left {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] (a : α) :
α ≃o α

equiv.add_left as an order_iso. See also order_embedding.add_left.

Equations
source
@[simp]
theorem order_iso.mul_left_apply {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] (a x : α) :
⇑(order_iso.mul_left a) x = a * x
source
def order_iso.mul_left {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] (a : α) :
α ≃o α

equiv.mul_left as an order_iso. See also order_embedding.mul_left.

Equations
source
@[simp]
theorem order_iso.mul_left_symm {α : Type u} [group α] [has_le α] [covariant_class α α has_mul.mul has_le.le] (a : α) :
(order_iso.mul_left a).symm = order_iso.mul_left a⁻¹
source
@[simp]
theorem order_iso.add_left_symm {α : Type u} [add_group α] [has_le α] [covariant_class α α has_add.add has_le.le] (a : α) :
(order_iso.add_left a).symm = order_iso.add_left (-a)
source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
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
source
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
source
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 - a → a + b ≤ c

Alias of le_sub_iff_add_le'.

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

Alias of le_sub_iff_add_le'.

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

Alias of sub_le_iff_le_add'.

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

Alias of sub_le_iff_le_add'.

source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
@[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
source
@[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
source
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
source
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
source
@[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
source
@[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
source
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 - b → b < a

Alias of sub_pos.

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

Alias of sub_pos.

source
@[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
source
@[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
source
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 < 0 → a < b

Alias of sub_neg.

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

Alias of sub_neg.

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

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

Alias of lt_sub_iff_add_lt.

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

Alias of lt_sub_iff_add_lt.

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

Alias of sub_lt_iff_lt_add.

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

Alias of sub_lt_iff_lt_add.

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

Alias of lt_sub_iff_add_lt'.

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

Alias of lt_sub_iff_add_lt'.

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

Alias of sub_lt_iff_lt_add'.

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

Alias of sub_lt_iff_lt_add'.

source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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
source
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 + ε
source
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 * ε
source
theorem sub_le_neg_add_iff {α : 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 ≤ -a + b ↔ a ≤ b
source
theorem div_le_inv_mul_iff {α : Type u} [group α] [linear_order α] [covariant_class α α has_mul.mul has_le.le] {a b : α} [covariant_class α α (function.swap has_mul.mul) has_le.le] :
a / b ≤ a⁻¹ * b ↔ a ≤ b
source
@[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
source
@[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
source
@[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
source
@[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
source
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.

source
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
source
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
source
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 : ∀ (ε : α), ε < 1 → a * ε ≤ b) :
a ≤ b
source
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 : ∀ (ε : α), ε < 0 → a + ε ≤ b) :
a ≤ b
source
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
source
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
source
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 + ε
source
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 * ε
source
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 ↔ ∀ (ε : α), ε < 0 → a + ε ≤ b
source
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 ↔ ∀ (ε : α), ε < 1 → a * ε ≤ b

Linearly ordered commutative groups #

source
@[instance]
def linear_ordered_add_comm_group.to_linear_order (α : Type u) [self : linear_ordered_add_comm_group α] :
linear_order α
source
@[instance]
def linear_ordered_add_comm_group.to_ordered_add_comm_group (α : Type u) [self : linear_ordered_add_comm_group α] :
ordered_add_comm_group α
source
@[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
source
@[instance]
def linear_ordered_add_comm_group_with_top.to_sub_neg_monoid (α : Type u_1) [self : linear_ordered_add_comm_group_with_top α] :
sub_neg_monoid α
source
@[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
source
@[instance]
def linear_ordered_add_comm_group_with_top.to_linear_ordered_add_comm_monoid_with_top (α : Type u_1) [self : linear_ordered_add_comm_group_with_top α] :
linear_ordered_add_comm_monoid_with_top α
source
@[instance]
def linear_ordered_add_comm_group_with_top.to_nontrivial (α : Type u_1) [self : linear_ordered_add_comm_group_with_top α] :
nontrivial α
source
@[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
source
@[instance]
def linear_ordered_comm_group.to_ordered_comm_group (α : Type u) [self : linear_ordered_comm_group α] :
ordered_comm_group α
source
@[instance]
def linear_ordered_comm_group.to_linear_order (α : Type u) [self : linear_ordered_comm_group α] :
linear_order α
source
@[protected, instance]
def order_dual.linear_ordered_comm_group {α : Type u} [linear_ordered_comm_group α] :
linear_ordered_comm_group (order_dual α)
Equations
source
@[protected, instance]
def order_dual.linear_ordered_add_comm_group {α : Type u} [linear_ordered_add_comm_group α] :
linear_ordered_add_comm_group (order_dual α)
Equations
source
@[protected, instance]
def linear_ordered_add_comm_group.to_linear_ordered_cancel_add_comm_monoid {α : Type u} [linear_ordered_add_comm_group α] :
linear_ordered_cancel_add_comm_monoid α
Equations
source
@[protected, instance]
def linear_ordered_comm_group.to_linear_ordered_cancel_comm_monoid {α : Type u} [linear_ordered_comm_group α] :
linear_ordered_cancel_comm_monoid α
Equations
source
def function.injective.linear_ordered_comm_group {α : Type u} [linear_ordered_comm_group α] {β : Type u_1} [has_one β] [has_mul β] [has_inv β] [has_div β] [has_pow β ℕ] [has_pow β ℤ] (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) (npow : ∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) (zpow : ∀ (x : β) (n : ℤ), f (x ^ n) = f x ^ n) :
linear_ordered_comm_group β

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

Equations
source
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 β] [has_scalar ℕ β] [has_scalar ℤ β] (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) (npow : ∀ (x : β) (n : ℕ), f (n • x) = n • f x) (zpow : ∀ (x : β) (n : ℤ), f (n • x) = n • f x) :
linear_ordered_add_comm_group β

Pullback a linear_ordered_add_comm_group under an injective map.

Equations
source
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
source
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
source
theorem min_neg_neg {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
min (-a) (-b) = -max a b
source
theorem min_inv_inv' {α : Type u} [linear_ordered_comm_group α] (a b : α) :
min a⁻¹ b⁻¹ = (max a b)⁻¹
source
theorem max_inv_inv' {α : Type u} [linear_ordered_comm_group α] (a b : α) :
max a⁻¹ b⁻¹ = (min a b)⁻¹
source
theorem max_neg_neg {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
max (-a) (-b) = -min a b
source
theorem min_div_div_right' {α : Type u} [linear_ordered_comm_group α] (a b c : α) :
min (a / c) (b / c) = min a b / c
source
theorem min_sub_sub_right {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
min (a - c) (b - c) = min a b - c
source
theorem max_div_div_right' {α : Type u} [linear_ordered_comm_group α] (a b c : α) :
max (a / c) (b / c) = max a b / c
source
theorem max_sub_sub_right {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
max (a - c) (b - c) = max a b - c
source
theorem min_div_div_left' {α : Type u} [linear_ordered_comm_group α] (a b c : α) :
min (a / b) (a / c) = a / max b c
source
theorem min_sub_sub_left {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
min (a - b) (a - c) = a - max b c
source
theorem max_div_div_left' {α : Type u} [linear_ordered_comm_group α] (a b c : α) :
max (a / b) (a / c) = a / min b c
source
theorem max_sub_sub_left {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
max (a - b) (a - c) = a - min b c
source
theorem eq_zero_of_neg_eq {α : Type u} [linear_ordered_add_comm_group α] {a : α} (h : -a = a) :
a = 0
source
theorem eq_one_of_inv_eq' {α : Type u} [linear_ordered_comm_group α] {a : α} (h : a⁻¹ = a) :
a = 1
source
theorem exists_one_lt' {α : Type u} [linear_ordered_comm_group α] [nontrivial α] :
∃ (a : α), 1 < a
source
theorem exists_zero_lt {α : Type u} [linear_ordered_add_comm_group α] [nontrivial α] :
∃ (a : α), 0 < a
source
@[protected, instance]
def linear_ordered_add_comm_group.to_no_max_order {α : Type u} [linear_ordered_add_comm_group α] [nontrivial α] :
no_max_order α
source
@[protected, instance]
def linear_ordered_comm_group.to_no_max_order {α : Type u} [linear_ordered_comm_group α] [nontrivial α] :
no_max_order α
source
@[protected, instance]
def linear_ordered_comm_group.to_no_min_order {α : Type u} [linear_ordered_comm_group α] [nontrivial α] :
no_min_order α
source
@[protected, instance]
def linear_ordered_add_comm_group.to_no_min_order {α : Type u} [linear_ordered_add_comm_group α] [nontrivial α] :
no_min_order α
source
@[protected, instance]
def has_neg.to_has_abs {α : Type u} [has_neg α] [has_sup α] :
has_abs α

abs a is the absolute value of a

Equations
source
@[protected, instance]
def has_inv.to_has_abs {α : Type u} [has_inv α] [has_sup α] :
has_abs α

abs a is the absolute value of a.

Equations
source
theorem abs_eq_sup_inv {α : Type u} [has_inv α] [has_sup α] (a : α) :
|a| = a ⊔ a⁻¹
source
theorem abs_eq_sup_neg {α : Type u} [has_neg α] [has_sup α] (a : α) :
|a| = a ⊔ -a
source
theorem abs_eq_max_neg {α : Type u} [has_neg α] [linear_order α] {a : α} :
|a| = max a (-a)
source
theorem abs_choice {α : Type u} [has_neg α] [linear_order α] (x : α) :
|x| = x ∨ |x| = -x
source
theorem abs_le' {α : Type u} [has_neg α] [linear_order α] {a b : α} :
|a| ≤ b ↔ a ≤ b ∧ -a ≤ b
source
theorem le_abs {α : Type u} [has_neg α] [linear_order α] {a b : α} :
a ≤ |b| ↔ a ≤ b ∨ a ≤ -b
source
theorem le_abs_self {α : Type u} [has_neg α] [linear_order α] (a : α) :
a ≤ |a|
source
theorem neg_le_abs_self {α : Type u} [has_neg α] [linear_order α] (a : α) :
-a ≤ |a|
source
theorem lt_abs {α : Type u} [has_neg α] [linear_order α] {a b : α} :
a < |b| ↔ a < b ∨ a < -b
source
theorem abs_le_abs {α : Type u} [has_neg α] [linear_order α] {a b : α} (h₀ : a ≤ b) (h₁ : -a ≤ b) :
|a| ≤ |b|
source
theorem abs_by_cases {α : Type u} [has_neg α] [linear_order α] (P : α → Prop) {a : α} (h1 : P a) (h2 : P (-a)) :
P |a|
source
@[simp]
theorem abs_neg {α : Type u} [add_group α] [linear_order α] (a : α) :
|-a| = |a|
source
theorem eq_or_eq_neg_of_abs_eq {α : Type u} [add_group α] [linear_order α] {a b : α} (h : |a| = b) :
a = b ∨ a = -b
source
theorem abs_eq_abs {α : Type u} [add_group α] [linear_order α] {a b : α} :
|a| = |b| ↔ a = b ∨ a = -b
source
theorem abs_sub_comm {α : Type u} [add_group α] [linear_order α] (a b : α) :
|a - b| = |b - a|
source
theorem abs_of_nonneg {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} (h : 0 ≤ a) :
|a| = a
source
theorem abs_of_pos {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} (h : 0 < a) :
|a| = a
source
theorem abs_of_nonpos {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} (h : a ≤ 0) :
|a| = -a
source
theorem abs_of_neg {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} (h : a < 0) :
|a| = -a
source
@[simp]
theorem abs_zero {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] :
|0| = 0
source
@[simp]
theorem abs_pos {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} :
0 < |a| ↔ a ≠ 0
source
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|
source
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|
source
theorem neg_abs_le_self {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] (a : α) :
-|a| ≤ a
source
theorem abs_nonneg {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] (a : α) :
0 ≤ |a|
source
@[simp]
theorem abs_abs {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] (a : α) :
||a|| = |a|
source
@[simp]
theorem abs_eq_zero {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} :
|a| = 0 ↔ a = 0
source
@[simp]
theorem abs_nonpos_iff {α : Type u} [add_group α] [linear_order α] [covariant_class α α has_add.add has_le.le] {a : α} :
|a| ≤ 0 ↔ a = 0
source
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
source
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
source
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
source
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 = |a - b|
source
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|
source
theorem abs_le {α : Type u} [linear_ordered_add_comm_group α] {a b : α} :
|a| ≤ b ↔ -b ≤ a ∧ a ≤ b
source
theorem le_abs' {α : Type u} [linear_ordered_add_comm_group α] {a b : α} :
a ≤ |b| ↔ b ≤ -a ∨ a ≤ b
source
theorem neg_le_of_abs_le {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h : |a| ≤ b) :
-b ≤ a
source
theorem le_of_abs_le {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h : |a| ≤ b) :
a ≤ b
source
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.

source
theorem abs_sub {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
|a - b| ≤ |a| + |b|
source
theorem abs_sub_le_iff {α : Type u} [linear_ordered_add_comm_group α] {a b c : α} :
|a - b| ≤ c ↔ a - b ≤ c ∧ b - a ≤ c
source
theorem abs_sub_lt_iff {α : Type u} [linear_ordered_add_comm_group α] {a b c : α} :
|a - b| < c ↔ a - b < c ∧ b - a < c
source
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
source
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
source
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
source
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
source
theorem abs_sub_abs_le_abs_sub {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
|a| - |b| ≤ |a - b|
source
theorem abs_abs_sub_abs_le_abs_sub {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
||a| - |b|| ≤ |a - b|
source
theorem abs_eq {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (hb : 0 ≤ b) :
|a| = b ↔ a = b ∨ a = -b
source
theorem abs_le_max_abs_abs {α : Type u} [linear_ordered_add_comm_group α] {a b c : α} (hab : a ≤ b) (hbc : b ≤ c) :
|b| ≤ max |a| |c|
source
theorem eq_of_abs_sub_eq_zero {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h : |a - b| = 0) :
a = b
source
theorem abs_sub_le {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
|a - c| ≤ |a - b| + |b - c|
source
theorem abs_add_three {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
|a + b + c| ≤ |a| + |b| + |c|
source
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
source
theorem eq_of_abs_sub_nonpos {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h : |a - b| ≤ 0) :
a = b
source
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)
source
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|
source
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|
source
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|
source
@[protected, instance]
def with_top.linear_ordered_add_comm_group_with_top {α : Type u} [linear_ordered_add_comm_group α] :
linear_ordered_add_comm_group_with_top (with_top α)
Equations
source
@[simp, norm_cast]
theorem with_top.coe_neg {α : Type u} [linear_ordered_add_comm_group α] (a : α) :
↑-a = -↑a
source
@[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 a → self.nonneg b → self.nonneg (a + b)
  • nonneg_antisymm : ∀ {a : α}, self.nonneg a → self.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.

source
def add_comm_group.total_positive_cone.to_positive_cone {α : Type u_1} [add_comm_group α] (self : add_comm_group.total_positive_cone α) :
add_comm_group.positive_cone α

Forget that a total_positive_cone is total.

source
@[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.

source
def ordered_add_comm_group.mk_of_positive_cone {α : Type u_1} [add_comm_group α] (C : add_comm_group.positive_cone α) :
ordered_add_comm_group α

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

Equations
source
def linear_ordered_add_comm_group.mk_of_positive_cone {α : Type u_1} [add_comm_group α] (C : add_comm_group.total_positive_cone α) :
linear_ordered_add_comm_group α

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
source
@[protected, instance]
def prod.ordered_comm_group {G : Type u_1} {H : Type u_2} [ordered_comm_group G] [ordered_comm_group H] :
ordered_comm_group (G × H)
Equations
source
@[protected, instance]
def prod.ordered_add_comm_group {G : Type u_1} {H : Type u_2} [ordered_add_comm_group G] [ordered_add_comm_group H] :
ordered_add_comm_group (G × H)
Equations
source
@[protected, instance]
def multiplicative.ordered_comm_group {α : Type u} [ordered_add_comm_group α] :
ordered_comm_group (multiplicative α)
Equations
source
@[protected, instance]
def additive.ordered_add_comm_group {α : Type u} [ordered_comm_group α] :
ordered_add_comm_group (additive α)
Equations
source
@[protected, instance]
def multiplicative.linear_ordered_comm_group {α : Type u} [linear_ordered_add_comm_group α] :
linear_ordered_comm_group (multiplicative α)
Equations
source
@[protected, instance]
def additive.linear_ordered_add_comm_group {α : Type u} [linear_ordered_comm_group α] :
linear_ordered_add_comm_group (additive α)
Equations
source
theorem neg_le_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :
a ≤ b → -b ≤ -a
source
theorem inv_le_inv' {α : Type u} [ordered_comm_group α] {a b : α} :
a ≤ b → b⁻¹ ≤ a⁻¹
source
theorem neg_lt_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :
a < b → -b < -a
source
theorem inv_lt_inv' {α : Type u} [ordered_comm_group α] {a b : α} :
a < b → b⁻¹ < a⁻¹
source
theorem inv_lt_one_of_one_lt {α : Type u} [ordered_comm_group α] {a : α} :
1 < a → a⁻¹ < 1
source
theorem neg_neg_of_pos {α : Type u} [ordered_add_comm_group α] {a : α} :
0 < a → -a < 0
source
theorem inv_le_one_of_one_le {α : Type u} [ordered_comm_group α] {a : α} :
1 ≤ a → a⁻¹ ≤ 1
source
theorem neg_nonpos_of_nonneg {α : Type u} [ordered_add_comm_group α] {a : α} :
0 ≤ a → -a ≤ 0
source
theorem one_le_inv_of_le_one {α : Type u} [ordered_comm_group α] {a : α} :
a ≤ 1 → 1 ≤ a⁻¹
source
theorem neg_nonneg_of_nonpos {α : Type u} [ordered_add_comm_group α] {a : α} :
a ≤ 0 → 0 ≤ -a