mathlib documentation

algebra.ordered_group

Ordered groups #

This file develops the basics of ordered groups.

Implementation details #

Unfortunately, the number of ' appended to lemmas in this file may differ between the multiplicative and the additive version of a lemma. The reason is that we did not want to change existing names in the library.

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 add_units.ordered_add_comm_group {α : Type u} [ordered_add_comm_monoid α] :
ordered_add_comm_group (add_units α)
source
@[protected, instance]
def units.ordered_comm_group {α : Type u} [ordered_comm_monoid α] :
ordered_comm_group (units α)

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

Equations
source
theorem ordered_comm_group.mul_lt_mul_left' {α : Type u} [ordered_comm_group α] (a b : α) (h : a < b) (c : α) :
c * a < c * b
source
theorem ordered_add_comm_group.add_lt_add_left {α : Type u} [ordered_add_comm_group α] (a b : α) (h : a < b) (c : α) :
c + a < c + b
source
theorem ordered_add_comm_group.le_of_add_le_add_left {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a + b ≤ a + c) :
b ≤ c
source
theorem ordered_comm_group.le_of_mul_le_mul_left {α : Type u} [ordered_comm_group α] {a b c : α} (h : a * b ≤ a * c) :
b ≤ c
source
theorem ordered_comm_group.lt_of_mul_lt_mul_left {α : Type u} [ordered_comm_group α] {a b c : α} (h : a * b < a * c) :
b < c
source
theorem ordered_add_comm_group.lt_of_add_lt_add_left {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a + b < a + c) :
b < c
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 α
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
theorem neg_le_neg {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a ≤ b) :
-b ≤ -a
source
theorem inv_le_inv' {α : Type u} [ordered_comm_group α] {a b : α} (h : a ≤ b) :
b⁻¹ ≤ a⁻¹
source
theorem le_of_neg_le_neg {α : Type u} [ordered_add_comm_group α] {a b : α} (h : -b ≤ -a) :
a ≤ b
source
theorem le_of_inv_le_inv {α : Type u} [ordered_comm_group α] {a b : α} (h : b⁻¹ ≤ a⁻¹) :
a ≤ b
source
theorem one_le_of_inv_le_one {α : Type u} [ordered_comm_group α] {a : α} (h : a⁻¹ ≤ 1) :
1 ≤ a
source
theorem nonneg_of_neg_nonpos {α : Type u} [ordered_add_comm_group α] {a : α} (h : -a ≤ 0) :
0 ≤ a
source
theorem inv_le_one_of_one_le {α : Type u} [ordered_comm_group α] {a : α} (h : 1 ≤ a) :
a⁻¹ ≤ 1
source
theorem neg_nonpos_of_nonneg {α : Type u} [ordered_add_comm_group α] {a : α} (h : 0 ≤ a) :
-a ≤ 0
source
theorem le_one_of_one_le_inv {α : Type u} [ordered_comm_group α] {a : α} (h : 1 ≤ a⁻¹) :
a ≤ 1
source
theorem nonpos_of_neg_nonneg {α : Type u} [ordered_add_comm_group α] {a : α} (h : 0 ≤ -a) :
a ≤ 0
source
theorem one_le_inv_of_le_one {α : Type u} [ordered_comm_group α] {a : α} (h : a ≤ 1) :
1 ≤ a⁻¹
source
theorem neg_nonneg_of_nonpos {α : Type u} [ordered_add_comm_group α] {a : α} (h : a ≤ 0) :
0 ≤ -a
source
theorem neg_lt_neg {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a < b) :
-b < -a
source
theorem inv_lt_inv' {α : Type u} [ordered_comm_group α] {a b : α} (h : a < b) :
b⁻¹ < a⁻¹
source
theorem lt_of_inv_lt_inv {α : Type u} [ordered_comm_group α] {a b : α} (h : b⁻¹ < a⁻¹) :
a < b
source
theorem lt_of_neg_lt_neg {α : Type u} [ordered_add_comm_group α] {a b : α} (h : -b < -a) :
a < b
source
theorem pos_of_neg_neg {α : Type u} [ordered_add_comm_group α] {a : α} (h : -a < 0) :
0 < a
source
theorem one_lt_of_inv_inv {α : Type u} [ordered_comm_group α] {a : α} (h : a⁻¹ < 1) :
1 < a
source
theorem inv_inv_of_one_lt {α : Type u} [ordered_comm_group α] {a : α} (h : 1 < a) :
a⁻¹ < 1
source
theorem neg_neg_of_pos {α : Type u} [ordered_add_comm_group α] {a : α} (h : 0 < a) :
-a < 0
source
theorem neg_of_neg_pos {α : Type u} [ordered_add_comm_group α] {a : α} (h : 0 < -a) :
a < 0
source
theorem inv_of_one_lt_inv {α : Type u} [ordered_comm_group α] {a : α} (h : 1 < a⁻¹) :
a < 1
source
theorem one_lt_inv_of_inv {α : Type u} [ordered_comm_group α] {a : α} (h : a < 1) :
1 < a⁻¹
source
theorem neg_pos_of_neg {α : Type u} [ordered_add_comm_group α] {a : α} (h : a < 0) :
0 < -a
source
theorem le_neg_of_le_neg {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a ≤ -b) :
b ≤ -a
source
theorem le_inv_of_le_inv {α : Type u} [ordered_comm_group α] {a b : α} (h : a ≤ b⁻¹) :
b ≤ a⁻¹
source
theorem inv_le_of_inv_le {α : Type u} [ordered_comm_group α] {a b : α} (h : a⁻¹ ≤ b) :
b⁻¹ ≤ a
source
theorem neg_le_of_neg_le {α : Type u} [ordered_add_comm_group α] {a b : α} (h : -a ≤ b) :
-b ≤ a
source
theorem lt_neg_of_lt_neg {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a < -b) :
b < -a
source
theorem lt_inv_of_lt_inv {α : Type u} [ordered_comm_group α] {a b : α} (h : a < b⁻¹) :
b < a⁻¹
source
theorem inv_lt_of_inv_lt {α : Type u} [ordered_comm_group α] {a b : α} (h : a⁻¹ < b) :
b⁻¹ < a
source
theorem neg_lt_of_neg_lt {α : Type u} [ordered_add_comm_group α] {a b : α} (h : -a < b) :
-b < a
source
theorem add_le_of_le_neg_add {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : b ≤ -a + c) :
a + b ≤ c
source
theorem mul_le_of_le_inv_mul {α : Type u} [ordered_comm_group α] {a b c : α} (h : b ≤ a⁻¹ * c) :
a * b ≤ c
source
theorem le_inv_mul_of_mul_le {α : Type u} [ordered_comm_group α] {a b c : α} (h : a * b ≤ c) :
b ≤ a⁻¹ * c
source
theorem le_neg_add_of_add_le {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a + b ≤ c) :
b ≤ -a + c
source
theorem le_mul_of_inv_mul_le {α : Type u} [ordered_comm_group α] {a b c : α} (h : b⁻¹ * a ≤ c) :
a ≤ b * c
source
theorem le_add_of_neg_add_le {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : -b + a ≤ c) :
a ≤ b + c
source
theorem neg_add_le_of_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a ≤ b + c) :
-b + a ≤ c
source
theorem inv_mul_le_of_le_mul {α : Type u} [ordered_comm_group α] {a b c : α} (h : a ≤ b * c) :
b⁻¹ * a ≤ c
source
theorem le_mul_of_inv_mul_le_left {α : Type u} [ordered_comm_group α] {a b c : α} (h : b⁻¹ * a ≤ c) :
a ≤ b * c
source
theorem le_add_of_neg_add_le_left {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : -b + a ≤ c) :
a ≤ b + c
source
theorem neg_add_le_left_of_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a ≤ b + c) :
-b + a ≤ c
source
theorem inv_mul_le_left_of_le_mul {α : Type u} [ordered_comm_group α] {a b c : α} (h : a ≤ b * c) :
b⁻¹ * a ≤ c
source
theorem le_mul_of_inv_mul_le_right {α : Type u} [ordered_comm_group α] {a b c : α} (h : c⁻¹ * a ≤ b) :
a ≤ b * c
source
theorem le_add_of_neg_add_le_right {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : -c + a ≤ b) :
a ≤ b + c
source
theorem neg_add_le_right_of_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a ≤ b + c) :
-c + a ≤ b
source
theorem inv_mul_le_right_of_le_mul {α : Type u} [ordered_comm_group α] {a b c : α} (h : a ≤ b * c) :
c⁻¹ * a ≤ b
source
theorem add_lt_of_lt_neg_add {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : b < -a + c) :
a + b < c
source
theorem mul_lt_of_lt_inv_mul {α : Type u} [ordered_comm_group α] {a b c : α} (h : b < a⁻¹ * c) :
a * b < c
source
theorem lt_inv_mul_of_mul_lt {α : Type u} [ordered_comm_group α] {a b c : α} (h : a * b < c) :
b < a⁻¹ * c
source
theorem lt_neg_add_of_add_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a + b < c) :
b < -a + c
source
theorem lt_add_of_neg_add_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : -b + a < c) :
a < b + c
source
theorem lt_mul_of_inv_mul_lt {α : Type u} [ordered_comm_group α] {a b c : α} (h : b⁻¹ * a < c) :
a < b * c
source
theorem neg_add_lt_of_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a < b + c) :
-b + a < c
source
theorem inv_mul_lt_of_lt_mul {α : Type u} [ordered_comm_group α] {a b c : α} (h : a < b * c) :
b⁻¹ * a < c
source
theorem lt_add_of_neg_add_lt_left {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : -b + a < c) :
a < b + c
source
theorem lt_mul_of_inv_mul_lt_left {α : Type u} [ordered_comm_group α] {a b c : α} (h : b⁻¹ * a < c) :
a < b * c
source
theorem inv_mul_lt_left_of_lt_mul {α : Type u} [ordered_comm_group α] {a b c : α} (h : a < b * c) :
b⁻¹ * a < c
source
theorem neg_add_lt_left_of_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a < b + c) :
-b + a < c
source
theorem lt_add_of_neg_add_lt_right {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : -c + a < b) :
a < b + c
source
theorem lt_mul_of_inv_mul_lt_right {α : Type u} [ordered_comm_group α] {a b c : α} (h : c⁻¹ * a < b) :
a < b * c
source
theorem inv_mul_lt_right_of_lt_mul {α : Type u} [ordered_comm_group α] {a b c : α} (h : a < b * c) :
c⁻¹ * a < b
source
theorem neg_add_lt_right_of_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a < b + c) :
-c + a < b
source
@[simp]
theorem inv_lt_one_iff_one_lt {α : Type u} [ordered_comm_group α] {a : α} :
a⁻¹ < 1 ↔ 1 < a
source
@[simp]
theorem neg_neg_iff_pos {α : Type u} [ordered_add_comm_group α] {a : α} :
-a < 0 ↔ 0 < a
source
@[simp]
theorem neg_le_neg_iff {α : Type u} [ordered_add_comm_group α] {a b : α} :
-a ≤ -b ↔ b ≤ a
source
@[simp]
theorem inv_le_inv_iff {α : Type u} [ordered_comm_group α] {a b : α} :
a⁻¹ ≤ b⁻¹ ↔ b ≤ a
source
theorem neg_le {α : Type u} [ordered_add_comm_group α] {a b : α} :
-a ≤ b ↔ -b ≤ a
source
theorem inv_le' {α : Type u} [ordered_comm_group α] {a b : α} :
a⁻¹ ≤ b ↔ b⁻¹ ≤ a
source
theorem le_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :
a ≤ -b ↔ b ≤ -a
source
theorem le_inv' {α : Type u} [ordered_comm_group α] {a b : α} :
a ≤ b⁻¹ ↔ b ≤ a⁻¹
source
theorem inv_le_iff_one_le_mul {α : Type u} [ordered_comm_group α] {a b : α} :
a⁻¹ ≤ b ↔ 1 ≤ b * a
source
theorem neg_le_iff_add_nonneg {α : Type u} [ordered_add_comm_group α] {a b : α} :
-a ≤ b ↔ 0 ≤ b + a
source
theorem inv_le_iff_one_le_mul' {α : Type u} [ordered_comm_group α] {a b : α} :
a⁻¹ ≤ b ↔ 1 ≤ a * b
source
theorem neg_le_iff_add_nonneg' {α : Type u} [ordered_add_comm_group α] {a b : α} :
-a ≤ b ↔ 0 ≤ a + b
source
theorem neg_lt_iff_pos_add {α : Type u} [ordered_add_comm_group α] {a b : α} :
-a < b ↔ 0 < b + a
source
theorem inv_lt_iff_one_lt_mul {α : Type u} [ordered_comm_group α] {a b : α} :
a⁻¹ < b ↔ 1 < b * a
source
theorem inv_lt_iff_one_lt_mul' {α : Type u} [ordered_comm_group α] {a b : α} :
a⁻¹ < b ↔ 1 < a * b
source
theorem neg_lt_iff_pos_add' {α : Type u} [ordered_add_comm_group α] {a b : α} :
-a < b ↔ 0 < a + b
source
theorem le_neg_iff_add_nonpos {α : Type u} [ordered_add_comm_group α] {a b : α} :
a ≤ -b ↔ a + b ≤ 0
source
theorem le_inv_iff_mul_le_one {α : Type u} [ordered_comm_group α] {a b : α} :
a ≤ b⁻¹ ↔ a * b ≤ 1
source
theorem le_inv_iff_mul_le_one' {α : Type u} [ordered_comm_group α] {a b : α} :
a ≤ b⁻¹ ↔ b * a ≤ 1
source
theorem le_neg_iff_add_nonpos' {α : Type u} [ordered_add_comm_group α] {a b : α} :
a ≤ -b ↔ b + a ≤ 0
source
theorem lt_inv_iff_mul_lt_one {α : Type u} [ordered_comm_group α] {a b : α} :
a < b⁻¹ ↔ a * b < 1
source
theorem lt_neg_iff_add_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :
a < -b ↔ a + b < 0
source
theorem lt_inv_iff_mul_lt_one' {α : Type u} [ordered_comm_group α] {a b : α} :
a < b⁻¹ ↔ b * a < 1
source
theorem lt_neg_iff_add_neg' {α : Type u} [ordered_add_comm_group α] {a b : α} :
a < -b ↔ b + a < 0
source
@[simp]
theorem neg_nonpos {α : Type u} [ordered_add_comm_group α] {a : α} :
-a ≤ 0 ↔ 0 ≤ a
source
@[simp]
theorem inv_le_one' {α : Type u} [ordered_comm_group α] {a : α} :
a⁻¹ ≤ 1 ↔ 1 ≤ a
source
@[simp]
theorem one_le_inv' {α : Type u} [ordered_comm_group α] {a : α} :
1 ≤ a⁻¹ ↔ a ≤ 1
source
@[simp]
theorem neg_nonneg {α : Type u} [ordered_add_comm_group α] {a : α} :
0 ≤ -a ↔ a ≤ 0
source
theorem inv_le_self {α : Type u} [ordered_comm_group α] {a : α} (h : 1 ≤ a) :
a⁻¹ ≤ a
source
theorem neg_le_self {α : Type u} [ordered_add_comm_group α] {a : α} (h : 0 ≤ a) :
-a ≤ a
source
theorem self_le_inv {α : Type u} [ordered_comm_group α] {a : α} (h : a ≤ 1) :
a ≤ a⁻¹
source
theorem self_le_neg {α : Type u} [ordered_add_comm_group α] {a : α} (h : a ≤ 0) :
a ≤ -a
source
@[simp]
theorem inv_lt_inv_iff {α : Type u} [ordered_comm_group α] {a b : α} :
a⁻¹ < b⁻¹ ↔ b < a
source
@[simp]
theorem neg_lt_neg_iff {α : Type u} [ordered_add_comm_group α] {a b : α} :
-a < -b ↔ b < a
source
theorem inv_lt_one' {α : Type u} [ordered_comm_group α] {a : α} :
a⁻¹ < 1 ↔ 1 < a
source
theorem neg_lt_zero {α : Type u} [ordered_add_comm_group α] {a : α} :
-a < 0 ↔ 0 < a
source
theorem neg_pos {α : Type u} [ordered_add_comm_group α] {a : α} :
0 < -a ↔ a < 0
source
theorem one_lt_inv' {α : Type u} [ordered_comm_group α] {a : α} :
1 < a⁻¹ ↔ a < 1
source
theorem neg_lt {α : Type u} [ordered_add_comm_group α] {a b : α} :
-a < b ↔ -b < a
source
theorem inv_lt' {α : Type u} [ordered_comm_group α] {a b : α} :
a⁻¹ < b ↔ b⁻¹ < a
source
theorem lt_inv' {α : Type u} [ordered_comm_group α] {a b : α} :
a < b⁻¹ ↔ b < a⁻¹
source
theorem lt_neg {α : Type u} [ordered_add_comm_group α] {a b : α} :
a < -b ↔ b < -a
source
theorem neg_lt_self {α : Type u} [ordered_add_comm_group α] {a : α} (h : 0 < a) :
-a < a
source
theorem inv_lt_self {α : Type u} [ordered_comm_group α] {a : α} (h : 1 < a) :
a⁻¹ < a
source
theorem le_neg_add_iff_add_le {α : Type u} [ordered_add_comm_group α] {a b c : α} :
b ≤ -a + c ↔ a + b ≤ c
source
theorem le_inv_mul_iff_mul_le {α : Type u} [ordered_comm_group α] {a b c : α} :
b ≤ a⁻¹ * c ↔ a * b ≤ c
source
@[simp]
theorem inv_mul_le_iff_le_mul {α : Type u} [ordered_comm_group α] {a b c : α} :
b⁻¹ * a ≤ c ↔ a ≤ b * c
source
@[simp]
theorem neg_add_le_iff_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :
-b + a ≤ c ↔ a ≤ b + c
source
theorem mul_inv_le_iff_le_mul {α : Type u} [ordered_comm_group α] {a b c : α} :
a * c⁻¹ ≤ b ↔ a ≤ b * c
source
theorem add_neg_le_iff_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a + -c ≤ b ↔ a ≤ b + c
source
@[simp]
theorem mul_inv_le_iff_le_mul' {α : Type u} [ordered_comm_group α] {a b c : α} :
a * b⁻¹ ≤ c ↔ a ≤ b * c
source
@[simp]
theorem add_neg_le_iff_le_add' {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a + -b ≤ c ↔ a ≤ b + c
source
theorem inv_mul_le_iff_le_mul' {α : Type u} [ordered_comm_group α] {a b c : α} :
c⁻¹ * a ≤ b ↔ a ≤ b * c
source
theorem neg_add_le_iff_le_add' {α : Type u} [ordered_add_comm_group α] {a b c : α} :
-c + a ≤ b ↔ a ≤ b + c
source
@[simp]
theorem lt_inv_mul_iff_mul_lt {α : Type u} [ordered_comm_group α] {a b c : α} :
b < a⁻¹ * c ↔ a * b < c
source
@[simp]
theorem lt_neg_add_iff_add_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :
b < -a + c ↔ a + b < c
source
@[simp]
theorem inv_mul_lt_iff_lt_mul {α : Type u} [ordered_comm_group α] {a b c : α} :
b⁻¹ * a < c ↔ a < b * c
source
@[simp]
theorem neg_add_lt_iff_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :
-b + a < c ↔ a < b + c
source
theorem neg_add_lt_iff_lt_add_right {α : Type u} [ordered_add_comm_group α] {a b c : α} :
-c + a < b ↔ a < b + c
source
theorem inv_mul_lt_iff_lt_mul_right {α : Type u} [ordered_comm_group α] {a b c : α} :
c⁻¹ * a < b ↔ a < b * c
source
theorem div_le_div_iff' {α : Type u} [ordered_comm_group α] {a b c d : α} :
a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b
source
theorem add_neg_le_add_neg_iff {α : Type u} [ordered_add_comm_group α] {a b c d : α} :
a + -b ≤ c + -d ↔ a + d ≤ c + b
source
@[simp]
theorem sub_le_self_iff {α : Type u} [ordered_add_comm_group α] (a : α) {b : α} :
a - b ≤ a ↔ 0 ≤ b
source
@[simp]
theorem div_le_self_iff {α : Type u} [ordered_comm_group α] (a : α) {b : α} :
a / b ≤ a ↔ 1 ≤ b
source
@[simp]
theorem div_lt_self_iff {α : Type u} [ordered_comm_group α] (a : α) {b : α} :
a / b < a ↔ 1 < b
source
@[simp]
theorem sub_lt_self_iff {α : Type u} [ordered_add_comm_group α] (a : α) {b : α} :
a - b < a ↔ 0 < b
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 β] (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) :
ordered_add_comm_group β

Pullback an ordered_add_comm_group under an injective map.

source
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) :
ordered_comm_group β

Pullback an ordered_comm_group under an injective map.

Equations
source
theorem sub_le_sub {α : Type u} [ordered_add_comm_group α] {a b c d : α} (hab : a ≤ b) (hcd : c ≤ d) :
a - d ≤ b - c
source
theorem sub_lt_sub {α : Type u} [ordered_add_comm_group α] {a b c d : α} (hab : a < b) (hcd : c < d) :
a - d < b - c
source
theorem sub_le_self {α : Type u} [ordered_add_comm_group α] (a : α) {b : α} :
0 ≤ b → a - b ≤ a

Alias of sub_le_self_iff.

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

Alias of sub_lt_self_iff.

source
theorem sub_le_sub_iff {α : Type u} [ordered_add_comm_group α] {a b c d : α} :
a - b ≤ c - d ↔ a + d ≤ c + b
source
@[simp]
theorem sub_le_sub_iff_left {α : Type u} [ordered_add_comm_group α] (a : α) {b c : α} :
a - b ≤ a - c ↔ c ≤ b
source
theorem sub_le_sub_left {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a ≤ b) (c : α) :
c - b ≤ c - a
source
@[simp]
theorem sub_le_sub_iff_right {α : Type u} [ordered_add_comm_group α] {a b : α} (c : α) :
a - c ≤ b - c ↔ a ≤ b
source
theorem sub_le_sub_right {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a ≤ b) (c : α) :
a - c ≤ b - c
source
@[simp]
theorem sub_lt_sub_iff_left {α : Type u} [ordered_add_comm_group α] (a : α) {b c : α} :
a - b < a - c ↔ c < b
source
theorem sub_lt_sub_left {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a < b) (c : α) :
c - b < c - a
source
@[simp]
theorem sub_lt_sub_iff_right {α : Type u} [ordered_add_comm_group α] {a b : α} (c : α) :
a - c < b - c ↔ a < b
source
theorem sub_lt_sub_right {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a < b) (c : α) :
a - c < b - c
source
@[simp]
theorem sub_nonneg {α : Type u} [ordered_add_comm_group α] {a b : α} :
0 ≤ a - b ↔ b ≤ a
source
theorem le_of_sub_nonneg {α : Type u} [ordered_add_comm_group α] {a b : α} :
0 ≤ a - b → b ≤ a

Alias of sub_nonneg.

source
theorem sub_nonneg_of_le {α : Type u} [ordered_add_comm_group α] {a b : α} :
b ≤ a → 0 ≤ a - b

Alias of sub_nonneg.

source
@[simp]
theorem sub_nonpos {α : Type u} [ordered_add_comm_group α] {a b : α} :
a - b ≤ 0 ↔ a ≤ b
source
theorem sub_nonpos_of_le {α : Type u} [ordered_add_comm_group α] {a b : α} :
a ≤ b → a - b ≤ 0

Alias of sub_nonpos.

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

Alias of sub_nonpos.

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

Alias of sub_pos.

source
theorem sub_pos_of_lt {α : Type u} [ordered_add_comm_group α] {a b : α} :
b < a → 0 < a - b

Alias of sub_pos.

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

Alias of sub_lt_zero.

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

Alias of sub_lt_zero.

source
theorem le_sub_iff_add_le' {α : Type u} [ordered_add_comm_group α] {a b c : α} :
b ≤ c - a ↔ a + b ≤ c
source
theorem le_sub_iff_add_le {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a ≤ c - b ↔ a + b ≤ c
source
theorem add_le_of_le_sub_right {α : Type u} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {a b c : α} :
a - b ≤ c ↔ a ≤ b + c
source
theorem add_le_of_le_sub_left {α : Type u} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {a b c : α} :
a - c ≤ b ↔ a ≤ b + c
source
@[simp]
theorem neg_le_sub_iff_le_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :
-b ≤ a - c ↔ c ≤ a + b
source
theorem neg_le_sub_iff_le_add' {α : Type u} [ordered_add_comm_group α] {a b c : α} :
-a ≤ b - c ↔ c ≤ a + b
source
theorem sub_le {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a - b ≤ c ↔ a - c ≤ b
source
theorem le_sub {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a ≤ b - c ↔ c ≤ b - a
source
theorem lt_sub_iff_add_lt' {α : Type u} [ordered_add_comm_group α] {a b c : α} :
b < c - a ↔ a + b < c
source
theorem add_lt_of_lt_sub_left {α : Type u} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {a b c : α} :
a + b < c → b < c - a

Alias of lt_sub_iff_add_lt'.

source
theorem lt_sub_iff_add_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a < c - b ↔ a + b < c
source
theorem add_lt_of_lt_sub_right {α : Type u} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {a b c : α} :
a - b < c ↔ a < b + c
source
theorem sub_left_lt_of_lt_add {α : Type u} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {a b c : α} :
a - b < c → a < b + c

Alias of sub_lt_iff_lt_add'.

source
theorem sub_lt_iff_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a - c < b ↔ a < b + c
source
theorem lt_add_of_sub_right_lt {α : Type u} [ordered_add_comm_group α] {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} [ordered_add_comm_group α] {a b c : α} :
a < b + c → a - c < b

Alias of sub_lt_iff_lt_add.

source
@[simp]
theorem neg_lt_sub_iff_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :
-b < a - c ↔ c < a + b
source
theorem neg_lt_sub_iff_lt_add' {α : Type u} [ordered_add_comm_group α] {a b c : α} :
-a < b - c ↔ c < a + b
source
theorem sub_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a - b < c ↔ a - c < b
source
theorem lt_sub {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a < b - c ↔ c < b - a

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_add_comm_group (α : Type u) [self : linear_ordered_add_comm_group α] :
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_comm_group (α : Type u) [self : linear_ordered_comm_group α] :
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 linear_ordered_comm_group.to_ordered_comm_group {α : Type u} [linear_ordered_comm_group α] :
ordered_comm_group α
Equations
source
@[protected, instance]
def linear_ordered_add_comm_group.to_ordered_add_comm_group {α : Type u} [linear_ordered_add_comm_group α] :
ordered_add_comm_group α
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 α
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 β] (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) :
linear_ordered_comm_group β

Pullback a linear_ordered_comm_group under an injective map.

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 β] (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) :
linear_ordered_add_comm_group β

Pullback a linear_ordered_add_comm_group under an injective map.

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 max_zero_sub_eq_self {α : Type u} [linear_ordered_add_comm_group α] (a : α) :
max a 0 - max (-a) 0 = a
source
theorem max_one_div_eq_self' {α : Type u} [linear_ordered_comm_group α] (a : α) :
max a 1 / max a⁻¹ 1 = a
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_comm_group.to_no_top_order {α : Type u} [linear_ordered_comm_group α] [nontrivial α] :
no_top_order α
source
@[protected, instance]
def linear_ordered_add_comm_group.to_no_top_order {α : Type u} [linear_ordered_add_comm_group α] [nontrivial α] :
no_top_order α
source
@[protected, instance]
def linear_ordered_add_comm_group.to_no_bot_order {α : Type u} [linear_ordered_add_comm_group α] [nontrivial α] :
no_bot_order α
source
@[protected, instance]
def linear_ordered_comm_group.to_no_bot_order {α : Type u} [linear_ordered_comm_group α] [nontrivial α] :
no_bot_order α
source
@[simp]
theorem sub_le_sub_flip {α : Type u} [linear_ordered_add_comm_group α] {a b : α} :
a - b ≤ b - a ↔ a ≤ b
source
theorem le_of_forall_pos_le_add {α : Type u} [linear_ordered_add_comm_group α] {a b : α} [densely_ordered α] (h : ∀ (ε : α), 0 < ε → a ≤ b + ε) :
a ≤ b
source
theorem le_iff_forall_pos_le_add {α : Type u} [linear_ordered_add_comm_group α] {a b : α} [densely_ordered α] :
a ≤ b ↔ ∀ (ε : α), 0 < ε → a ≤ b + ε
source
theorem le_of_forall_pos_lt_add {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h : ∀ (ε : α), 0 < ε → a < b + ε) :
a ≤ b
source
theorem le_iff_forall_pos_lt_add {α : Type u} [linear_ordered_add_comm_group α] {a b : α} :
a ≤ b ↔ ∀ (ε : α), 0 < ε → a < b + ε
source
def abs {α : Type u} [linear_ordered_add_comm_group α] (a : α) :
α

abs a is the absolute value of a.

Equations
source
theorem abs_of_nonneg {α : Type u} [linear_ordered_add_comm_group α] {a : α} (h : 0 ≤ a) :
abs a = a
source
theorem abs_of_pos {α : Type u} [linear_ordered_add_comm_group α] {a : α} (h : 0 < a) :
abs a = a
source
theorem abs_of_nonpos {α : Type u} [linear_ordered_add_comm_group α] {a : α} (h : a ≤ 0) :
abs a = -a
source
theorem abs_of_neg {α : Type u} [linear_ordered_add_comm_group α] {a : α} (h : a < 0) :
abs a = -a
source
@[simp]
theorem abs_zero {α : Type u} [linear_ordered_add_comm_group α] :
abs 0 = 0
source
@[simp]
theorem abs_neg {α : Type u} [linear_ordered_add_comm_group α] (a : α) :
abs (-a) = abs a
source
@[simp]
theorem abs_pos {α : Type u} [linear_ordered_add_comm_group α] {a : α} :
0 < abs a ↔ a ≠ 0
source
theorem abs_pos_of_pos {α : Type u} [linear_ordered_add_comm_group α] {a : α} (h : 0 < a) :
0 < abs a
source
theorem abs_pos_of_neg {α : Type u} [linear_ordered_add_comm_group α] {a : α} (h : a < 0) :
0 < abs a
source
theorem abs_sub {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
abs (a - b) = abs (b - a)
source
theorem abs_le' {α : Type u} [linear_ordered_add_comm_group α] {a b : α} :
abs a ≤ b ↔ a ≤ b ∧ -a ≤ b
source
theorem abs_le {α : Type u} [linear_ordered_add_comm_group α] {a b : α} :
abs a ≤ b ↔ -b ≤ a ∧ a ≤ b
source
theorem neg_le_of_abs_le {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h : abs a ≤ b) :
-b ≤ a
source
theorem le_of_abs_le {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h : abs a ≤ b) :
a ≤ b
source
theorem le_abs {α : Type u} [linear_ordered_add_comm_group α] {a b : α} :
a ≤ abs b ↔ a ≤ b ∨ a ≤ -b
source
theorem le_abs_self {α : Type u} [linear_ordered_add_comm_group α] (a : α) :
a ≤ abs a
source
theorem neg_le_abs_self {α : Type u} [linear_ordered_add_comm_group α] (a : α) :
-a ≤ abs a
source
theorem abs_nonneg {α : Type u} [linear_ordered_add_comm_group α] (a : α) :
0 ≤ abs a
source
@[simp]
theorem abs_abs {α : Type u} [linear_ordered_add_comm_group α] (a : α) :
abs (abs a) = abs a
source
@[simp]
theorem abs_eq_zero {α : Type u} [linear_ordered_add_comm_group α] {a : α} :
abs a = 0 ↔ a = 0
source
@[simp]
theorem abs_nonpos_iff {α : Type u} [linear_ordered_add_comm_group α] {a : α} :
abs a ≤ 0 ↔ a = 0
source
theorem abs_lt {α : Type u} [linear_ordered_add_comm_group α] {a b : α} :
abs a < b ↔ -b < a ∧ a < b
source
theorem neg_lt_of_abs_lt {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h : abs a < b) :
-b < a
source
theorem lt_of_abs_lt {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h : abs a < b) :
a < b
source
theorem lt_abs {α : Type u} [linear_ordered_add_comm_group α] {a b : α} :
a < abs b ↔ a < b ∨ a < -b
source
theorem max_sub_min_eq_abs' {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
max a b - min a b = abs (a - b)
source
theorem max_sub_min_eq_abs {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
max a b - min a b = abs (b - a)
source
theorem abs_add {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
abs (a + b) ≤ abs a + abs b
source
theorem abs_sub_le_iff {α : Type u} [linear_ordered_add_comm_group α] {a b c : α} :
abs (a - b) ≤ c ↔ a - b ≤ c ∧ b - a ≤ c
source
theorem abs_sub_lt_iff {α : Type u} [linear_ordered_add_comm_group α] {a b c : α} :
abs (a - b) < c ↔ a - b < c ∧ b - a < c
source
theorem sub_le_of_abs_sub_le_left {α : Type u} [linear_ordered_add_comm_group α] {a b c : α} (h : abs (a - b) ≤ c) :
b - c ≤ a
source
theorem sub_le_of_abs_sub_le_right {α : Type u} [linear_ordered_add_comm_group α] {a b c : α} (h : abs (a - b) ≤ c) :
a - c ≤ b
source
theorem sub_lt_of_abs_sub_lt_left {α : Type u} [linear_ordered_add_comm_group α] {a b c : α} (h : abs (a - b) < c) :
b - c < a
source
theorem sub_lt_of_abs_sub_lt_right {α : Type u} [linear_ordered_add_comm_group α] {a b c : α} (h : abs (a - b) < c) :
a - c < b
source
theorem abs_sub_abs_le_abs_sub {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
abs a - abs b ≤ abs (a - b)
source
theorem abs_abs_sub_abs_le_abs_sub {α : Type u} [linear_ordered_add_comm_group α] (a b : α) :
abs (abs a - abs b) ≤ abs (a - b)
source
theorem abs_eq {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (hb : 0 ≤ b) :
abs 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) :
abs b ≤ max (abs a) (abs c)
source
theorem abs_le_abs {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h₀ : a ≤ b) (h₁ : -a ≤ b) :
abs a ≤ abs b
source
theorem abs_max_sub_max_le_abs {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
abs (max a c - max b c) ≤ abs (a - b)
source
theorem eq_of_abs_sub_eq_zero {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h : abs (a - b) = 0) :
a = b
source
theorem abs_by_cases {α : Type u} [linear_ordered_add_comm_group α] (P : α → Prop) {a : α} (h1 : P a) (h2 : P (-a)) :
P (abs a)
source
theorem abs_sub_le {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
abs (a - c) ≤ abs (a - b) + abs (b - c)
source
theorem abs_add_three {α : Type u} [linear_ordered_add_comm_group α] (a b c : α) :
abs (a + b + c) ≤ abs a + abs b + abs 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) :
abs (a - b) ≤ ub - lb
source
theorem eq_of_abs_sub_nonpos {α : Type u} [linear_ordered_add_comm_group α] {a b : α} (h : abs (a - b) ≤ 0) :
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
@[instance]
def nonneg_add_comm_group.to_add_comm_group (α : Type u_1) [self : nonneg_add_comm_group α] :
add_comm_group α
source
@[class]
structure nonneg_add_comm_group (α : Type u_1) :
Type u_1

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

Instances
source
@[protected, instance]
def nonneg_add_comm_group.to_ordered_add_comm_group {α : Type u} [s : nonneg_add_comm_group α] :
ordered_add_comm_group α
Equations
source
theorem nonneg_add_comm_group.nonneg_def {α : Type u} [s : nonneg_add_comm_group α] {a : α} :
nonneg_add_comm_group.nonneg a ↔ 0 ≤ a
source
theorem nonneg_add_comm_group.pos_def {α : Type u} [s : nonneg_add_comm_group α] {a : α} :
nonneg_add_comm_group.pos a ↔ 0 < a
source
theorem nonneg_add_comm_group.not_zero_pos {α : Type u} [s : nonneg_add_comm_group α] :
¬nonneg_add_comm_group.pos 0
source
theorem nonneg_add_comm_group.zero_lt_iff_nonneg_nonneg {α : Type u} [s : nonneg_add_comm_group α] {a : α} :
0 < a ↔ nonneg_add_comm_group.nonneg a ∧ ¬nonneg_add_comm_group.nonneg (-a)
source
theorem nonneg_add_comm_group.nonneg_total_iff {α : Type u} [s : nonneg_add_comm_group α] :
(∀ (a : α), nonneg_add_comm_group.nonneg a ∨ nonneg_add_comm_group.nonneg (-a)) ↔ ∀ (a b : α), a ≤ b ∨ b ≤ a
source
def nonneg_add_comm_group.to_linear_ordered_add_comm_group {α : Type u} [s : nonneg_add_comm_group α] [decidable_pred nonneg_add_comm_group.nonneg] (nonneg_total : ∀ (a : α), nonneg_add_comm_group.nonneg a ∨ nonneg_add_comm_group.nonneg (-a)) :
linear_ordered_add_comm_group α

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

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.linear_ordered_add_comm_group {α : Type u} [linear_ordered_add_comm_group α] :
linear_ordered_add_comm_group (order_dual α)
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)
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