mathlib documentation

algebra.ordered_group

Ordered monoids and groups

This file develops the basics of ordered monoids and 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_comm_monoid.to_comm_monoid (α : Type u_1) [s : ordered_comm_monoid α] :
comm_monoid α

source
@[instance]
def ordered_comm_monoid.to_partial_order (α : Type u_1) [s : ordered_comm_monoid α] :
partial_order α

source
@[class]
structure ordered_comm_monoid (α : Type u_1) :
Type u_1
  • mul : α → α → α
  • mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • mul_comm : ∀ (a b : α), a * b = b * a
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b
  • lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1 → b < c_1

An ordered commutative monoid is a commutative monoid with a partial order such that

  • a ≤ b → c * a ≤ c * b (multiplication is monotone)
  • a * b < a * c → b < c.
Instances
source
@[instance]
def ordered_add_comm_monoid.to_partial_order (α : Type u_1) [s : ordered_add_comm_monoid α] :
partial_order α

source
@[instance]
def ordered_add_comm_monoid.to_add_comm_monoid (α : Type u_1) [s : ordered_add_comm_monoid α] :
add_comm_monoid α

source
@[class]
structure ordered_add_comm_monoid (α : Type u_1) :
Type u_1
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • add_comm : ∀ (a b : α), a + b = b + a
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
  • lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < c_1

An ordered (additive) commutative monoid is a commutative monoid with a partial order such that

  • a ≤ b → c + a ≤ c + b (addition is monotone)
  • a + b < a + c → b < c.
Instances
source
theorem mul_le_mul_left' {α : Type u} [ordered_comm_monoid α] {a b : α} (h : a ≤ b) (c : α) :
c * a ≤ c * b

source
theorem add_le_add_left {α : Type u} [ordered_add_comm_monoid α] {a b : α} (h : a ≤ b) (c : α) :
c + a ≤ c + b

source
theorem add_le_add_right {α : Type u} [ordered_add_comm_monoid α] {a b : α} (h : a ≤ b) (c : α) :
a + c ≤ b + c

source
theorem mul_le_mul_right' {α : Type u} [ordered_comm_monoid α] {a b : α} (h : a ≤ b) (c : α) :
a * c ≤ b * c

source
theorem lt_of_add_lt_add_left {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (a_1 : a + b < a + c) :
b < c

source
theorem lt_of_mul_lt_mul_left' {α : Type u} [ordered_comm_monoid α] {a b c : α} (a_1 : a * b < a * c) :
b < c

source
theorem add_le_add {α : Type u} [ordered_add_comm_monoid α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :
a + c ≤ b + d

source
theorem mul_le_mul' {α : Type u} [ordered_comm_monoid α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c ≤ d) :
a * c ≤ b * d

source
theorem mul_le_mul_three {α : Type u} [ordered_comm_monoid α] {a b c d e f : α} (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) :
(a * b) * c ≤ (d * e) * f

source
theorem add_le_add_three {α : Type u} [ordered_add_comm_monoid α] {a b c d e f : α} (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) :
a + b + c ≤ d + e + f

source
theorem le_add_of_nonneg_right {α : Type u} [ordered_add_comm_monoid α] {a b : α} (h : 0 ≤ b) :
a ≤ a + b

source
theorem le_mul_of_one_le_right' {α : Type u} [ordered_comm_monoid α] {a b : α} (h : 1 ≤ b) :
a ≤ a * b

source
theorem le_mul_of_one_le_left' {α : Type u} [ordered_comm_monoid α] {a b : α} (h : 1 ≤ b) :
a ≤ b * a

source
theorem le_add_of_nonneg_left {α : Type u} [ordered_add_comm_monoid α] {a b : α} (h : 0 ≤ b) :
a ≤ b + a

source
theorem lt_of_add_lt_add_right {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (h : a + b < c + b) :
a < c

source
theorem lt_of_mul_lt_mul_right' {α : Type u} [ordered_comm_monoid α] {a b c : α} (h : a * b < c * b) :
a < c

source
theorem le_add_of_nonneg_of_le {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (ha : 0 ≤ a) (hbc : b ≤ c) :
b ≤ a + c

source
theorem le_mul_of_one_le_of_le {α : Type u} [ordered_comm_monoid α] {a b c : α} (ha : 1 ≤ a) (hbc : b ≤ c) :
b ≤ a * c

source
theorem le_add_of_le_of_nonneg {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : 0 ≤ a) :
b ≤ c + a

source
theorem le_mul_of_le_of_one_le {α : Type u} [ordered_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : 1 ≤ a) :
b ≤ c * a

source
theorem one_le_mul {α : Type u} [ordered_comm_monoid α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) :
1 ≤ a * b

source
theorem add_nonneg {α : Type u} [ordered_add_comm_monoid α] {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) :
0 ≤ a + b

source
theorem one_lt_mul_of_lt_of_le' {α : Type u} [ordered_comm_monoid α] {a b : α} (ha : 1 < a) (hb : 1 ≤ b) :
1 < a * b

source
theorem add_pos_of_pos_of_nonneg {α : Type u} [ordered_add_comm_monoid α] {a b : α} (ha : 0 < a) (hb : 0 ≤ b) :
0 < a + b

source
theorem add_pos_of_nonneg_of_pos {α : Type u} [ordered_add_comm_monoid α] {a b : α} (ha : 0 ≤ a) (hb : 0 < b) :
0 < a + b

source
theorem one_lt_mul_of_le_of_lt' {α : Type u} [ordered_comm_monoid α] {a b : α} (ha : 1 ≤ a) (hb : 1 < b) :
1 < a * b

source
theorem one_lt_mul' {α : Type u} [ordered_comm_monoid α] {a b : α} (ha : 1 < a) (hb : 1 < b) :
1 < a * b

source
theorem add_pos {α : Type u} [ordered_add_comm_monoid α] {a b : α} (ha : 0 < a) (hb : 0 < b) :
0 < a + b

source
theorem add_nonpos {α : Type u} [ordered_add_comm_monoid α] {a b : α} (ha : a ≤ 0) (hb : b ≤ 0) :
a + b ≤ 0

source
theorem mul_le_one' {α : Type u} [ordered_comm_monoid α] {a b : α} (ha : a ≤ 1) (hb : b ≤ 1) :
a * b ≤ 1

source
theorem mul_le_of_le_one_of_le' {α : Type u} [ordered_comm_monoid α] {a b c : α} (ha : a ≤ 1) (hbc : b ≤ c) :
a * b ≤ c

source
theorem add_le_of_nonpos_of_le' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (ha : a ≤ 0) (hbc : b ≤ c) :
a + b ≤ c

source
theorem add_le_of_le_of_nonpos' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : a ≤ 0) :
b + a ≤ c

source
theorem mul_le_of_le_of_le_one' {α : Type u} [ordered_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : a ≤ 1) :
b * a ≤ c

source
theorem add_neg_of_neg_of_nonpos' {α : Type u} [ordered_add_comm_monoid α] {a b : α} (ha : a < 0) (hb : b ≤ 0) :
a + b < 0

source
theorem mul_lt_one_of_lt_one_of_le_one' {α : Type u} [ordered_comm_monoid α] {a b : α} (ha : a < 1) (hb : b ≤ 1) :
a * b < 1

source
theorem mul_lt_one_of_le_one_of_lt_one' {α : Type u} [ordered_comm_monoid α] {a b : α} (ha : a ≤ 1) (hb : b < 1) :
a * b < 1

source
theorem add_neg_of_nonpos_of_neg' {α : Type u} [ordered_add_comm_monoid α] {a b : α} (ha : a ≤ 0) (hb : b < 0) :
a + b < 0

source
theorem mul_lt_one' {α : Type u} [ordered_comm_monoid α] {a b : α} (ha : a < 1) (hb : b < 1) :
a * b < 1

source
theorem add_neg' {α : Type u} [ordered_add_comm_monoid α] {a b : α} (ha : a < 0) (hb : b < 0) :
a + b < 0

source
theorem lt_mul_of_one_le_of_lt' {α : Type u} [ordered_comm_monoid α] {a b c : α} (ha : 1 ≤ a) (hbc : b < c) :
b < a * c

source
theorem lt_add_of_nonneg_of_lt' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (ha : 0 ≤ a) (hbc : b < c) :
b < a + c

source
theorem lt_mul_of_lt_of_one_le' {α : Type u} [ordered_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 1 ≤ a) :
b < c * a

source
theorem lt_add_of_lt_of_nonneg' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 0 ≤ a) :
b < c + a

source
theorem lt_add_of_pos_of_lt' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (ha : 0 < a) (hbc : b < c) :
b < a + c

source
theorem lt_mul_of_one_lt_of_lt' {α : Type u} [ordered_comm_monoid α] {a b c : α} (ha : 1 < a) (hbc : b < c) :
b < a * c

source
theorem lt_add_of_lt_of_pos' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 0 < a) :
b < c + a

source
theorem lt_mul_of_lt_of_one_lt' {α : Type u} [ordered_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 1 < a) :
b < c * a

source
theorem add_lt_of_nonpos_of_lt' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (ha : a ≤ 0) (hbc : b < c) :
a + b < c

source
theorem mul_lt_of_le_one_of_lt' {α : Type u} [ordered_comm_monoid α] {a b c : α} (ha : a ≤ 1) (hbc : b < c) :
a * b < c

source
theorem mul_lt_of_lt_of_le_one' {α : Type u} [ordered_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a ≤ 1) :
b * a < c

source
theorem add_lt_of_lt_of_nonpos' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a ≤ 0) :
b + a < c

source
theorem mul_lt_of_lt_one_of_lt' {α : Type u} [ordered_comm_monoid α] {a b c : α} (ha : a < 1) (hbc : b < c) :
a * b < c

source
theorem add_lt_of_neg_of_lt' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (ha : a < 0) (hbc : b < c) :
a + b < c

source
theorem mul_lt_of_lt_of_lt_one' {α : Type u} [ordered_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a < 1) :
b * a < c

source
theorem add_lt_of_lt_of_neg' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a < 0) :
b + a < c

source
theorem add_eq_zero_iff' {α : Type u} [ordered_add_comm_monoid α] {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) :
a + b = 0 ↔ a = 0 ∧ b = 0

source
theorem mul_eq_one_iff' {α : Type u} [ordered_comm_monoid α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) :
a * b = 1 ↔ a = 1 ∧ b = 1

source
theorem monotone.mul' {α : Type u} [ordered_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} (hf : monotone f) (hg : monotone g) :
monotone (λ (x : β), (f x) * g x)

source
theorem monotone.add {α : Type u} [ordered_add_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} (hf : monotone f) (hg : monotone g) :
monotone (λ (x : β), f x + g x)

source
theorem monotone.add_const {α : Type u} [ordered_add_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : monotone f) (a : α) :
monotone (λ (x : β), f x + a)

source
theorem monotone.mul_const' {α : Type u} [ordered_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : monotone f) (a : α) :
monotone (λ (x : β), (f x) * a)

source
theorem monotone.const_add {α : Type u} [ordered_add_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : monotone f) (a : α) :
monotone (λ (x : β), a + f x)

source
theorem monotone.const_mul' {α : Type u} [ordered_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : monotone f) (a : α) :
monotone (λ (x : β), a * f x)

source
theorem bit0_pos {α : Type u} [ordered_add_comm_monoid α] {a : α} (h : 0 < a) :
0 < bit0 a

source
@[instance]
def add_units.preorder {α : Type u} [add_monoid α] [preorder α] :
preorder (add_units α)

source
@[instance]
def units.preorder {α : Type u} [monoid α] [preorder α] :
preorder (units α)

Equations
source
@[simp]
theorem add_units.coe_le_coe {α : Type u} [add_monoid α] [preorder α] {a b : add_units α} :
↑a ≤ ↑b ↔ a ≤ b

source
@[simp]
theorem units.coe_le_coe {α : Type u} [monoid α] [preorder α] {a b : units α} :
↑a ≤ ↑b ↔ a ≤ b

source
@[simp]
theorem add_units.coe_lt_coe {α : Type u} [add_monoid α] [preorder α] {a b : add_units α} :
↑a < ↑b ↔ a < b

source
@[simp]
theorem units.coe_lt_coe {α : Type u} [monoid α] [preorder α] {a b : units α} :
↑a < ↑b ↔ a < b

source
@[instance]
def add_units.partial_order {α : Type u} [add_monoid α] [partial_order α] :
partial_order (add_units α)

source
@[instance]
def units.partial_order {α : Type u} [monoid α] [partial_order α] :
partial_order (units α)

Equations
source
@[instance]
def units.linear_order {α : Type u} [monoid α] [linear_order α] :
linear_order (units α)

Equations
source
@[instance]
def add_units.linear_order {α : Type u} [add_monoid α] [linear_order α] :
linear_order (add_units α)

source
@[instance]
def add_units.decidable_linear_order {α : Type u} [add_monoid α] [decidable_linear_order α] :
decidable_linear_order (add_units α)

source
@[instance]
def units.decidable_linear_order {α : Type u} [monoid α] [decidable_linear_order α] :
decidable_linear_order (units α)

Equations
source
@[simp]
theorem add_units.max_coe {α : Type u} [add_monoid α] [decidable_linear_order α] {a b : add_units α} :
↑(max a b) = max ↑a ↑b

source
@[simp]
theorem units.max_coe {α : Type u} [monoid α] [decidable_linear_order α] {a b : units α} :
↑(max a b) = max ↑a ↑b

source
@[simp]
theorem units.min_coe {α : Type u} [monoid α] [decidable_linear_order α] {a b : units α} :
↑(min a b) = min ↑a ↑b

source
@[simp]
theorem add_units.min_coe {α : Type u} [add_monoid α] [decidable_linear_order α] {a b : add_units α} :
↑(min a b) = min ↑a ↑b

source
@[instance]
def with_zero.preorder {α : Type u} [preorder α] :
preorder (with_zero α)

Equations
source
@[instance]
def with_zero.partial_order {α : Type u} [partial_order α] :
partial_order (with_zero α)

Equations
source
@[instance]
def with_zero.order_bot {α : Type u} [partial_order α] :
order_bot (with_zero α)

Equations
source
theorem with_zero.zero_le {α : Type u} [partial_order α] (a : with_zero α) :
0 ≤ a

source
theorem with_zero.zero_lt_coe {α : Type u} [partial_order α] (a : α) :
0 < ↑a

source
@[simp]
theorem with_zero.coe_lt_coe {α : Type u} [partial_order α] {a b : α} :
↑a < ↑b ↔ a < b

source
@[simp]
theorem with_zero.coe_le_coe {α : Type u} [partial_order α] {a b : α} :
↑a ≤ ↑b ↔ a ≤ b

source
@[instance]
def with_zero.lattice {α : Type u} [lattice α] :
lattice (with_zero α)

Equations
source
@[instance]
def with_zero.linear_order {α : Type u} [linear_order α] :
linear_order (with_zero α)

Equations
source
@[instance]
def with_zero.decidable_linear_order {α : Type u} [decidable_linear_order α] :
decidable_linear_order (with_zero α)

Equations
source
theorem with_zero.mul_le_mul_left {α : Type u} [ordered_comm_monoid α] (a b : with_zero α) (a_1 : a ≤ b) (c : with_zero α) :
c * a ≤ c * b

source
theorem with_zero.lt_of_mul_lt_mul_left {α : Type u} [ordered_comm_monoid α] (a b c : with_zero α) (a_1 : a * b < a * c) :
b < c

source
@[instance]
def with_zero.ordered_comm_monoid {α : Type u} [ordered_comm_monoid α] :
ordered_comm_monoid (with_zero α)

Equations
source
def with_zero.ordered_add_comm_monoid {α : Type u} [ordered_add_comm_monoid α] (zero_le : ∀ (a : α), 0 ≤ a) :
ordered_add_comm_monoid (with_zero α)

If 0 is the least element in α, then with_zero α is an ordered_add_comm_monoid.

Equations
source
@[instance]
def with_top.has_one {α : Type u} [has_one α] :
has_one (with_top α)

Equations
source
@[instance]
def with_top.has_zero {α : Type u} [has_zero α] :
has_zero (with_top α)

source
@[simp]
theorem with_top.coe_one {α : Type u} [has_one α] :
↑1 = 1

source
@[simp]
theorem with_top.coe_zero {α : Type u} [has_zero α] :
↑0 = 0

source
@[simp]
theorem with_top.coe_eq_zero {α : Type u} [has_zero α] {a : α} :
↑a = 0 ↔ a = 0

source
@[simp]
theorem with_top.coe_eq_one {α : Type u} [has_one α] {a : α} :
↑a = 1 ↔ a = 1

source
@[simp]
theorem with_top.zero_eq_coe {α : Type u} [has_zero α] {a : α} :
0 = ↑a ↔ a = 0

source
@[simp]
theorem with_top.one_eq_coe {α : Type u} [has_one α] {a : α} :
1 = ↑a ↔ a = 1

source
@[simp]
theorem with_top.top_ne_one {α : Type u} [has_one α] :
⊤ ≠ 1

source
@[simp]
theorem with_top.top_ne_zero {α : Type u} [has_zero α] :
⊤ ≠ 0

source
@[simp]
theorem with_top.zero_ne_top {α : Type u} [has_zero α] :
0 ≠ ⊤

source
@[simp]
theorem with_top.one_ne_top {α : Type u} [has_one α] :
1 ≠ ⊤

source
@[instance]
def with_top.has_add {α : Type u} [has_add α] :
has_add (with_top α)

Equations
source
@[instance]
def with_top.add_semigroup {α : Type u} [add_semigroup α] :
add_semigroup (with_top α)

Equations
source
theorem with_top.coe_add {α : Type u} [has_add α] {a b : α} :
↑(a + b) = ↑a + ↑b

source
theorem with_top.coe_bit0 {α : Type u} [has_add α] {a : α} :
↑(bit0 a) = bit0 ↑a

source
theorem with_top.coe_bit1 {α : Type u} [has_add α] [has_one α] {a : α} :
↑(bit1 a) = bit1 ↑a

source
@[instance]
def with_top.add_comm_semigroup {α : Type u} [add_comm_semigroup α] :
add_comm_semigroup (with_top α)

Equations
source
@[instance]
def with_top.add_monoid {α : Type u} [add_monoid α] :
add_monoid (with_top α)

Equations
source
@[instance]
def with_top.add_comm_monoid {α : Type u} [add_comm_monoid α] :
add_comm_monoid (with_top α)

Equations
source
@[instance]
def with_top.ordered_add_comm_monoid {α : Type u} [ordered_add_comm_monoid α] :
ordered_add_comm_monoid (with_top α)

Equations
source
@[simp]
theorem with_top.zero_lt_top {α : Type u} [ordered_add_comm_monoid α] :
0 < ⊤

source
@[simp]
theorem with_top.zero_lt_coe {α : Type u} [ordered_add_comm_monoid α] (a : α) :
0 < ↑a ↔ 0 < a

source
@[simp]
theorem with_top.add_top {α : Type u} [ordered_add_comm_monoid α] {a : with_top α} :
a + ⊤ = ⊤

source
@[simp]
theorem with_top.top_add {α : Type u} [ordered_add_comm_monoid α] {a : with_top α} :
⊤ + a = ⊤

source
theorem with_top.add_eq_top {α : Type u} [ordered_add_comm_monoid α] (a b : with_top α) :
a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤

source
theorem with_top.add_lt_top {α : Type u} [ordered_add_comm_monoid α] (a b : with_top α) :
a + b < ⊤ ↔ a < ⊤ ∧ b < ⊤

source
@[instance]
def with_bot.has_zero {α : Type u} [has_zero α] :
has_zero (with_bot α)

Equations
source
@[instance]
def with_bot.has_one {α : Type u} [has_one α] :
has_one (with_bot α)

Equations
source
@[instance]
def with_bot.add_semigroup {α : Type u} [add_semigroup α] :
add_semigroup (with_bot α)

Equations
source
@[instance]
def with_bot.add_comm_semigroup {α : Type u} [add_comm_semigroup α] :
add_comm_semigroup (with_bot α)

Equations
source
@[instance]
def with_bot.add_monoid {α : Type u} [add_monoid α] :
add_monoid (with_bot α)

Equations
source
@[instance]
def with_bot.add_comm_monoid {α : Type u} [add_comm_monoid α] :
add_comm_monoid (with_bot α)

Equations
source
@[instance]
def with_bot.ordered_add_comm_monoid {α : Type u} [ordered_add_comm_monoid α] :
ordered_add_comm_monoid (with_bot α)

Equations
source
theorem with_bot.coe_zero {α : Type u} [has_zero α] :
↑0 = 0

source
theorem with_bot.coe_one {α : Type u} [has_one α] :
↑1 = 1

source
theorem with_bot.coe_eq_zero {α : Type u_1} [add_monoid α] {a : α} :
↑a = 0 ↔ a = 0

source
theorem with_bot.coe_add {α : Type u} [add_semigroup α] (a b : α) :
↑(a + b) = ↑a + ↑b

source
theorem with_bot.coe_bit0 {α : Type u} [add_semigroup α] {a : α} :
↑(bit0 a) = bit0 ↑a

source
theorem with_bot.coe_bit1 {α : Type u} [add_semigroup α] [has_one α] {a : α} :
↑(bit1 a) = bit1 ↑a

source
@[simp]
theorem with_bot.bot_add {α : Type u} [ordered_add_comm_monoid α] (a : with_bot α) :
⊥ + a = ⊥

source
@[simp]
theorem with_bot.add_bot {α : Type u} [ordered_add_comm_monoid α] (a : with_bot α) :
a + ⊥ = ⊥

source
@[instance]
def canonically_ordered_add_monoid.to_ordered_add_comm_monoid (α : Type u_1) [s : canonically_ordered_add_monoid α] :
ordered_add_comm_monoid α

source
@[instance]
def canonically_ordered_add_monoid.to_order_bot (α : Type u_1) [s : canonically_ordered_add_monoid α] :
order_bot α

source
@[class]
structure canonically_ordered_add_monoid (α : Type u_1) :
Type u_1
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • add_comm : ∀ (a b : α), a + b = b + a
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
  • lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < c_1
  • bot : α
  • bot_le : ∀ (a : α), ⊥ ≤ a
  • le_iff_exists_add : ∀ (a b : α), a ≤ b ↔ ∃ (c_1 : α), b = a + c_1

A canonically ordered additive monoid is an ordered commutative additive monoid in which the ordering coincides with the divisibility relation, which is to say, a ≤ b iff there exists c with b = a + c. This is satisfied by the natural numbers, for example, but not the integers or other ordered groups.

Instances
source
theorem le_iff_exists_add {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :
a ≤ b ↔ ∃ (c : α), b = a + c

source
@[simp]
theorem zero_le {α : Type u} [canonically_ordered_add_monoid α] (a : α) :
0 ≤ a

source
@[simp]
theorem bot_eq_zero {α : Type u} [canonically_ordered_add_monoid α] :
⊥ = 0

source
@[simp]
theorem add_eq_zero_iff {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :
a + b = 0 ↔ a = 0 ∧ b = 0

source
@[simp]
theorem le_zero_iff_eq {α : Type u} [canonically_ordered_add_monoid α] {a : α} :
a ≤ 0 ↔ a = 0

source
theorem zero_lt_iff_ne_zero {α : Type u} [canonically_ordered_add_monoid α] {a : α} :
0 < a ↔ a ≠ 0

source
theorem exists_pos_add_of_lt {α : Type u} [canonically_ordered_add_monoid α] {a b : α} (h : a < b) :
∃ (c : α) (H : c > 0), a + c = b

source
theorem le_add_left {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} (h : a ≤ c) :
a ≤ b + c

source
theorem le_add_right {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} (h : a ≤ b) :
a ≤ b + c

source
@[instance]
def with_zero.canonically_ordered_add_monoid {α : Type u} [canonically_ordered_add_monoid α] :
canonically_ordered_add_monoid (with_zero α)

Equations
source
@[instance]
def with_top.canonically_ordered_add_monoid {α : Type u} [canonically_ordered_add_monoid α] :
canonically_ordered_add_monoid (with_top α)

Equations
source
@[instance]
def canonically_linear_ordered_add_monoid.to_decidable_linear_order (α : Type u_1) [s : canonically_linear_ordered_add_monoid α] :
decidable_linear_order α

source
@[instance]
def canonically_linear_ordered_add_monoid.to_canonically_ordered_add_monoid (α : Type u_1) [s : canonically_linear_ordered_add_monoid α] :
canonically_ordered_add_monoid α

source
@[class]
structure canonically_linear_ordered_add_monoid (α : Type u_1) :
Type u_1
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • add_comm : ∀ (a b : α), a + b = b + a
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
  • lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1 → b < c_1
  • bot : α
  • bot_le : ∀ (a : α), ⊥ ≤ a
  • le_iff_exists_add : ∀ (a b : α), a ≤ b ↔ ∃ (c_1 : α), b = a + c_1
  • le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
  • decidable_le : decidable_rel has_le.le
  • decidable_eq : decidable_eq α
  • decidable_lt : decidable_rel has_lt.lt

A canonically linear-ordered additive monoid is a canonically ordered additive monoid whose ordering is a decidable linear order.

source
@[instance]
def canonically_linear_ordered_add_monoid.semilattice_sup_bot {α : Type u} [canonically_linear_ordered_add_monoid α] :
semilattice_sup_bot α

Equations
source
@[class]
structure ordered_cancel_add_comm_monoid (α : Type u) :
Type u
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • add_comm : ∀ (a b : α), a + b = b + a
  • add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1 → b = c_1
  • add_right_cancel : ∀ (a b c_1 : α), a + b = c_1 + b → a = c_1
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
  • le_of_add_le_add_left : ∀ (a b c_1 : α), a + b ≤ a + c_1 → b ≤ c_1

An ordered cancellative additive commutative monoid is an additive commutative monoid with a partial order, in which addition is cancellative and strictly monotone.

Instances
source
@[instance]
def ordered_cancel_add_comm_monoid.to_add_comm_monoid (α : Type u) [s : ordered_cancel_add_comm_monoid α] :
add_comm_monoid α

source
@[instance]
def ordered_cancel_add_comm_monoid.to_partial_order (α : Type u) [s : ordered_cancel_add_comm_monoid α] :
partial_order α

source
@[instance]
def ordered_cancel_add_comm_monoid.to_add_right_cancel_semigroup (α : Type u) [s : ordered_cancel_add_comm_monoid α] :
add_right_cancel_semigroup α

source
@[instance]
def ordered_cancel_add_comm_monoid.to_add_left_cancel_semigroup (α : Type u) [s : ordered_cancel_add_comm_monoid α] :
add_left_cancel_semigroup α

source
@[instance]
def ordered_cancel_comm_monoid.to_partial_order (α : Type u) [s : ordered_cancel_comm_monoid α] :
partial_order α

source
@[instance]
def ordered_cancel_comm_monoid.to_left_cancel_semigroup (α : Type u) [s : ordered_cancel_comm_monoid α] :
left_cancel_semigroup α

source
@[instance]
def ordered_cancel_comm_monoid.to_comm_monoid (α : Type u) [s : ordered_cancel_comm_monoid α] :
comm_monoid α

source
@[class]
structure ordered_cancel_comm_monoid (α : Type u) :
Type u
  • mul : α → α → α
  • mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • mul_comm : ∀ (a b : α), a * b = b * a
  • mul_left_cancel : ∀ (a b c_1 : α), a * b = a * c_1 → b = c_1
  • mul_right_cancel : ∀ (a b c_1 : α), a * b = c_1 * b → a = c_1
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b
  • le_of_mul_le_mul_left : ∀ (a b c_1 : α), a * b ≤ a * c_1 → b ≤ c_1

An ordered cancellative commutative monoid is a commutative monoid with a partial order, in which multiplication is cancellative and strictly monotone.

Instances
source
@[instance]
def ordered_cancel_comm_monoid.to_right_cancel_semigroup (α : Type u) [s : ordered_cancel_comm_monoid α] :
right_cancel_semigroup α

source
@[instance]
def ordered_cancel_add_comm_monoid.to_left_cancel_add_monoid {α : Type u} [ordered_cancel_add_comm_monoid α] :
add_left_cancel_monoid α

source
@[instance]
def ordered_cancel_comm_monoid.to_left_cancel_monoid {α : Type u} [ordered_cancel_comm_monoid α] :
left_cancel_monoid α

Equations
source
theorem le_of_mul_le_mul_left' {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (a_1 : a * b ≤ a * c) :
b ≤ c

source
theorem le_of_add_le_add_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (a_1 : a + b ≤ a + c) :
b ≤ c

source
@[instance]
def ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid {α : Type u} [ordered_cancel_add_comm_monoid α] :
ordered_add_comm_monoid α

source
@[instance]
def ordered_cancel_comm_monoid.to_ordered_comm_monoid {α : Type u} [ordered_cancel_comm_monoid α] :
ordered_comm_monoid α

Equations
source
theorem add_lt_add_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (h : a < b) (c : α) :
c + a < c + b

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

source
theorem mul_lt_mul_right' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (h : a < b) (c : α) :
a * c < b * c

source
theorem add_lt_add_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (h : a < b) (c : α) :
a + c < b + c

source
theorem mul_lt_mul''' {α : Type u} [ordered_cancel_comm_monoid α] {a b c d : α} (h₁ : a < b) (h₂ : c < d) :
a * c < b * d

source
theorem add_lt_add {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c d : α} (h₁ : a < b) (h₂ : c < d) :
a + c < b + d

source
theorem mul_lt_mul_of_le_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c < d) :
a * c < b * d

source
theorem add_lt_add_of_le_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c d : α} (h₁ : a ≤ b) (h₂ : c < d) :
a + c < b + d

source
theorem add_lt_add_of_lt_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c d : α} (h₁ : a < b) (h₂ : c ≤ d) :
a + c < b + d

source
theorem mul_lt_mul_of_lt_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c d : α} (h₁ : a < b) (h₂ : c ≤ d) :
a * c < b * d

source
theorem lt_add_of_pos_right {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} (h : 0 < b) :
a < a + b

source
theorem lt_mul_of_one_lt_right' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} (h : 1 < b) :
a < a * b

source
theorem lt_add_of_pos_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} (h : 0 < b) :
a < b + a

source
theorem lt_mul_of_one_lt_left' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} (h : 1 < b) :
a < b * a

source
theorem le_of_mul_le_mul_right' {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (h : a * b ≤ c * b) :
a ≤ c

source
theorem le_of_add_le_add_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (h : a + b ≤ c + b) :
a ≤ c

source
theorem mul_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (ha : a < 1) (hb : b < 1) :
a * b < 1

source
theorem add_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (ha : a < 0) (hb : b < 0) :
a + b < 0

source
theorem add_neg_of_neg_of_nonpos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (ha : a < 0) (hb : b ≤ 0) :
a + b < 0

source
theorem mul_lt_one_of_lt_one_of_le_one {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (ha : a < 1) (hb : b ≤ 1) :
a * b < 1

source
theorem mul_lt_one_of_le_one_of_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (ha : a ≤ 1) (hb : b < 1) :
a * b < 1

source
theorem add_neg_of_nonpos_of_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (ha : a ≤ 0) (hb : b < 0) :
a + b < 0

source
theorem lt_add_of_pos_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : 0 < a) (hbc : b ≤ c) :
b < a + c

source
theorem lt_mul_of_one_lt_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : 1 < a) (hbc : b ≤ c) :
b < a * c

source
theorem lt_add_of_le_of_pos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : 0 < a) :
b < c + a

source
theorem lt_mul_of_le_of_one_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : 1 < a) :
b < c * a

source
theorem add_le_of_nonpos_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : a ≤ 0) (hbc : b ≤ c) :
a + b ≤ c

source
theorem mul_le_of_le_one_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : a ≤ 1) (hbc : b ≤ c) :
a * b ≤ c

source
theorem mul_le_of_le_of_le_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : a ≤ 1) :
b * a ≤ c

source
theorem add_le_of_le_of_nonpos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : a ≤ 0) :
b + a ≤ c

source
theorem mul_lt_of_lt_one_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : a < 1) (hbc : b ≤ c) :
a * b < c

source
theorem add_lt_of_neg_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : a < 0) (hbc : b ≤ c) :
a + b < c

source
theorem add_lt_of_le_of_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : a < 0) :
b + a < c

source
theorem mul_lt_of_le_of_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b ≤ c) (ha : a < 1) :
b * a < c

source
theorem lt_mul_of_one_le_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : 1 ≤ a) (hbc : b < c) :
b < a * c

source
theorem lt_add_of_nonneg_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : 0 ≤ a) (hbc : b < c) :
b < a + c

source
theorem lt_mul_of_lt_of_one_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 1 ≤ a) :
b < c * a

source
theorem lt_add_of_lt_of_nonneg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 0 ≤ a) :
b < c + a

source
theorem lt_mul_of_one_lt_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : 1 < a) (hbc : b < c) :
b < a * c

source
theorem lt_add_of_pos_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : 0 < a) (hbc : b < c) :
b < a + c

source
theorem lt_mul_of_lt_of_one_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 1 < a) :
b < c * a

source
theorem lt_add_of_lt_of_pos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : 0 < a) :
b < c + a

source
theorem mul_lt_of_le_one_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : a ≤ 1) (hbc : b < c) :
a * b < c

source
theorem add_lt_of_nonpos_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : a ≤ 0) (hbc : b < c) :
a + b < c

source
theorem add_lt_of_lt_of_nonpos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a ≤ 0) :
b + a < c

source
theorem mul_lt_of_lt_of_le_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a ≤ 1) :
b * a < c

source
theorem add_lt_of_neg_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (ha : a < 0) (hbc : b < c) :
a + b < c

source
theorem mul_lt_of_lt_one_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (ha : a < 1) (hbc : b < c) :
a * b < c

source
theorem mul_lt_of_lt_of_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a < 1) :
b * a < c

source
theorem add_lt_of_lt_of_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} (hbc : b < c) (ha : a < 0) :
b + a < c

source
@[simp]
theorem mul_le_mul_iff_left {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b c : α} :
a * b ≤ a * c ↔ b ≤ c

source
@[simp]
theorem add_le_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b c : α} :
a + b ≤ a + c ↔ b ≤ c

source
@[simp]
theorem mul_le_mul_iff_right {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (c : α) :
a * c ≤ b * c ↔ a ≤ b

source
@[simp]
theorem add_le_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (c : α) :
a + c ≤ b + c ↔ a ≤ b

source
@[simp]
theorem mul_lt_mul_iff_left {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b c : α} :
a * b < a * c ↔ b < c

source
@[simp]
theorem add_lt_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b c : α} :
a + b < a + c ↔ b < c

source
@[simp]
theorem mul_lt_mul_iff_right {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (c : α) :
a * c < b * c ↔ a < b

source
@[simp]
theorem add_lt_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (c : α) :
a + c < b + c ↔ a < b

source
@[simp]
theorem le_add_iff_nonneg_right {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} :
a ≤ a + b ↔ 0 ≤ b

source
@[simp]
theorem le_mul_iff_one_le_right' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} :
a ≤ a * b ↔ 1 ≤ b

source
@[simp]
theorem le_add_iff_nonneg_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} :
a ≤ b + a ↔ 0 ≤ b

source
@[simp]
theorem le_mul_iff_one_le_left' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} :
a ≤ b * a ↔ 1 ≤ b

source
@[simp]
theorem lt_add_iff_pos_right {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} :
a < a + b ↔ 0 < b

source
@[simp]
theorem lt_mul_iff_one_lt_right' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} :
a < a * b ↔ 1 < b

source
@[simp]
theorem lt_add_iff_pos_left {α : Type u} [ordered_cancel_add_comm_monoid α] (a : α) {b : α} :
a < b + a ↔ 0 < b

source
@[simp]
theorem lt_mul_iff_one_lt_left' {α : Type u} [ordered_cancel_comm_monoid α] (a : α) {b : α} :
a < b * a ↔ 1 < b

source
@[simp]
theorem add_le_iff_nonpos_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :
a + b ≤ b ↔ a ≤ 0

source
@[simp]
theorem mul_le_iff_le_one_left' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :
a * b ≤ b ↔ a ≤ 1

source
@[simp]
theorem add_le_iff_nonpos_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :
a + b ≤ a ↔ b ≤ 0

source
@[simp]
theorem mul_le_iff_le_one_right' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :
a * b ≤ a ↔ b ≤ 1

source
@[simp]
theorem add_lt_iff_neg_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :
a + b < b ↔ a < 0

source
@[simp]
theorem mul_lt_iff_lt_one_right' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :
a * b < b ↔ a < 1

source
@[simp]
theorem add_lt_iff_neg_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :
a + b < a ↔ b < 0

source
@[simp]
theorem mul_lt_iff_lt_one_left' {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :
a * b < a ↔ b < 1

source
theorem mul_eq_one_iff_eq_one_of_one_le {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) :
a * b = 1 ↔ a = 1 ∧ b = 1

source
theorem add_eq_zero_iff_eq_zero_of_nonneg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} (ha : 0 ≤ a) (hb : 0 ≤ b) :
a + b = 0 ↔ a = 0 ∧ b = 0

source
theorem monotone.mul_strict_mono' {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} (hf : monotone f) (hg : strict_mono g) :
strict_mono (λ (x : β), (f x) * g x)

source
theorem monotone.add_strict_mono {α : Type u} [ordered_cancel_add_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} (hf : monotone f) (hg : strict_mono g) :
strict_mono (λ (x : β), f x + g x)

source
theorem strict_mono.add_monotone {α : Type u} [ordered_cancel_add_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} (hf : strict_mono f) (hg : monotone g) :
strict_mono (λ (x : β), f x + g x)

source
theorem strict_mono.mul_monotone' {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [preorder β] {f g : β → α} (hf : strict_mono f) (hg : monotone g) :
strict_mono (λ (x : β), (f x) * g x)

source
theorem strict_mono.add_const {α : Type u} [ordered_cancel_add_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), f x + c)

source
theorem strict_mono.mul_const' {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), (f x) * c)

source
theorem strict_mono.const_add {α : Type u} [ordered_cancel_add_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), c + f x)

source
theorem strict_mono.const_mul' {α : Type u} [ordered_cancel_comm_monoid α] {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), c * f x)

source
theorem with_top.add_lt_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_top α} (a_1 : a < ⊤) :
a + c < a + b ↔ c < b

source
theorem with_top.add_lt_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_top α} (a_1 : a < ⊤) :
c + a < b + a ↔ c < b

source
@[instance]
def ordered_add_comm_group.to_partial_order (α : Type u) [s : ordered_add_comm_group α] :
partial_order α

source
@[class]
structure ordered_add_comm_group (α : Type u) :
Type u
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • neg : α → α
  • add_left_neg : ∀ (a : α), -a + a = 0
  • add_comm : ∀ (a b : α), a + b = b + a
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b

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

Instances
source
@[instance]
def ordered_add_comm_group.to_add_comm_group (α : Type u) [s : ordered_add_comm_group α] :
add_comm_group α

source
@[instance]
def ordered_comm_group.to_comm_group (α : Type u) [s : ordered_comm_group α] :
comm_group α

source
@[class]
structure ordered_comm_group (α : Type u) :
Type u
  • mul : α → α → α
  • mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
  • one : α
  • one_mul : ∀ (a : α), 1 * a = a
  • mul_one : ∀ (a : α), a * 1 = a
  • inv : α → α
  • mul_left_inv : ∀ (a : α), a⁻¹ * a = 1
  • mul_comm : ∀ (a b : α), a * b = b * a
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 * a ≤ c_1 * b

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

Instances
source
@[instance]
def ordered_comm_group.to_partial_order (α : Type u) [s : ordered_comm_group α] :
partial_order α

source
@[instance]
def add_units.ordered_add_comm_group {α : Type u} [ordered_add_comm_monoid α] :
ordered_add_comm_group (add_units α)

source
@[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
@[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
@[instance]
def ordered_comm_group.to_ordered_cancel_comm_monoid (α : Type u) [s : ordered_comm_group α] :
ordered_cancel_comm_monoid α

Equations
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 ≤ a * b

source
theorem neg_le_iff_add_nonneg {α : 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
@[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 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 sub_le_sub_iff {α : Type u} [ordered_add_comm_group α] (a b c d : α) :
a + -b ≤ c + -d ↔ a + d ≤ c + b

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 sub_nonneg_of_le {α : Type u} [ordered_add_comm_group α] {a b : α} (h : b ≤ a) :
0 ≤ a - b

source
theorem le_of_sub_nonneg {α : Type u} [ordered_add_comm_group α] {a b : α} (h : 0 ≤ a - b) :
b ≤ a

source
theorem sub_nonpos_of_le {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a ≤ b) :
a - b ≤ 0

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

source
theorem sub_le_of_sub_le {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a - b ≤ c) :
a - 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
theorem sub_le_sub_right {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a ≤ b) (c : α) :
a - c ≤ b - c

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 add_lt_of_lt_sub_left {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : b < c - a) :
a + b < c

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

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

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

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

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

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

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

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

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

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

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

source
theorem sub_lt_of_sub_lt {α : Type u} [ordered_add_comm_group α] {a b c : α} (h : a - b < c) :
a - 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
theorem sub_lt_sub_right {α : Type u} [ordered_add_comm_group α] {a b : α} (h : a < b) (c : α) :
a - c < 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_lt_sub_of_le_of_lt {α : 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_of_lt_of_le {α : 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 : α} (h : 0 ≤ b) :
a - b ≤ a

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

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

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

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

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

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

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

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

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

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 sub_le_iff_le_add' {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a - b ≤ c ↔ a ≤ b + c

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

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_lt_iff_lt_add {α : Type u} [ordered_add_comm_group α] {a b c : α} :
a - c < b ↔ a < b + c

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

source
theorem sub_le_self_iff {α : Type u} [ordered_add_comm_group α] (a : α) {b : α} :
a - b ≤ a ↔ 0 ≤ b

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

source
def ordered_comm_group.mk' {α : Type u} [comm_group α] [partial_order α] (mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c * a ≤ c * b) :
ordered_comm_group α

Alternative constructor for ordered commutative groups, that avoids the field mul_lt_mul_left.

Equations
source
def ordered_add_comm_group.mk' {α : Type u} [add_comm_group α] [partial_order α] (mul_le_mul_left : ∀ (a b : α), a ≤ b → ∀ (c : α), c + a ≤ c + b) :
ordered_add_comm_group α

Alternative constructor for ordered commutative groups, that avoids the field mul_lt_mul_left.

source
@[instance]
def decidable_linear_ordered_cancel_add_comm_monoid.to_decidable_linear_order (α : Type u) [s : decidable_linear_ordered_cancel_add_comm_monoid α] :
decidable_linear_order α

source
@[instance]
def decidable_linear_ordered_cancel_add_comm_monoid.to_ordered_cancel_add_comm_monoid (α : Type u) [s : decidable_linear_ordered_cancel_add_comm_monoid α] :
ordered_cancel_add_comm_monoid α

source
@[class]
structure decidable_linear_ordered_cancel_add_comm_monoid (α : Type u) :
Type u
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • add_comm : ∀ (a b : α), a + b = b + a
  • add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1 → b = c_1
  • add_right_cancel : ∀ (a b c_1 : α), a + b = c_1 + b → a = c_1
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b
  • le_of_add_le_add_left : ∀ (a b c_1 : α), a + b ≤ a + c_1 → b ≤ c_1
  • le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
  • decidable_le : decidable_rel has_le.le
  • decidable_eq : decidable_eq α
  • decidable_lt : decidable_rel has_lt.lt

A decidable linearly ordered cancellative additive commutative monoid is an additive commutative monoid with a decidable linear order in which addition is cancellative and strictly monotone.

Instances
source
theorem min_add_add_left {α : Type u} [decidable_linear_ordered_cancel_add_comm_monoid α] (a b c : α) :
min (a + b) (a + c) = a + min b c

source
theorem min_add_add_right {α : Type u} [decidable_linear_ordered_cancel_add_comm_monoid α] (a b c : α) :
min (a + c) (b + c) = min a b + c

source
theorem max_add_add_left {α : Type u} [decidable_linear_ordered_cancel_add_comm_monoid α] (a b c : α) :
max (a + b) (a + c) = a + max b c

source
theorem max_add_add_right {α : Type u} [decidable_linear_ordered_cancel_add_comm_monoid α] (a b c : α) :
max (a + c) (b + c) = max a b + c

source
@[instance]
def decidable_linear_ordered_add_comm_group.to_add_comm_group (α : Type u) [s : decidable_linear_ordered_add_comm_group α] :
add_comm_group α

source
@[instance]
def decidable_linear_ordered_add_comm_group.to_decidable_linear_order (α : Type u) [s : decidable_linear_ordered_add_comm_group α] :
decidable_linear_order α

source
@[class]
structure decidable_linear_ordered_add_comm_group (α : Type u) :
Type u
  • add : α → α → α
  • add_assoc : ∀ (a b c_1 : α), a + b + c_1 = a + (b + c_1)
  • zero : α
  • zero_add : ∀ (a : α), 0 + a = a
  • add_zero : ∀ (a : α), a + 0 = a
  • neg : α → α
  • add_left_neg : ∀ (a : α), -a + a = 0
  • add_comm : ∀ (a b : α), a + b = b + a
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a ≤ a
  • le_trans : ∀ (a b c_1 : α), a ≤ b → b ≤ c_1 → a ≤ c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
  • le_total : ∀ (a b : α), a ≤ b ∨ b ≤ a
  • decidable_le : decidable_rel has_le.le
  • decidable_eq : decidable_eq α
  • decidable_lt : decidable_rel has_lt.lt
  • add_le_add_left : ∀ (a b : α), a ≤ b → ∀ (c_1 : α), c_1 + a ≤ c_1 + b

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

Instances
source
@[instance]
def decidable_linear_ordered_comm_group.to_ordered_add_comm_group (α : Type u) [s : decidable_linear_ordered_add_comm_group α] :
ordered_add_comm_group α

Equations
source
@[instance]
def decidable_linear_ordered_add_comm_group.to_decidable_linear_ordered_cancel_add_comm_monoid {α : Type u} [decidable_linear_ordered_add_comm_group α] :
decidable_linear_ordered_cancel_add_comm_monoid α

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

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

source
theorem min_eq_neg_max_neg_neg {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b : α) :
min a b = -max (-a) (-b)

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

source
theorem max_eq_neg_min_neg_neg {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b : α) :
max a b = -min (-a) (-b)

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

abs a is the absolute value of a.

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

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

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

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

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

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

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

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

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

source
theorem ne_zero_of_abs_ne_zero {α : Type u} [decidable_linear_ordered_add_comm_group α] {a : α} (h : abs a ≠ 0) :
a ≠ 0

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

source
theorem abs_nonneg {α : Type u} [decidable_linear_ordered_add_comm_group α] (a : α) :
0 ≤ abs a

source
theorem abs_abs {α : Type u} [decidable_linear_ordered_add_comm_group α] (a : α) :
abs (abs a) = abs a

source
theorem le_abs_self {α : Type u} [decidable_linear_ordered_add_comm_group α] (a : α) :
a ≤ abs a

source
theorem neg_le_abs_self {α : Type u} [decidable_linear_ordered_add_comm_group α] (a : α) :
-a ≤ abs a

source
theorem eq_zero_of_abs_eq_zero {α : Type u} [decidable_linear_ordered_add_comm_group α] {a : α} (h : abs a = 0) :
a = 0

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

source
theorem abs_pos_of_ne_zero {α : Type u} [decidable_linear_ordered_add_comm_group α] {a : α} (h : a ≠ 0) :
0 < abs a

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

source
theorem abs_le_of_le_of_neg_le {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b : α} (h1 : a ≤ b) (h2 : -a ≤ b) :
abs a ≤ b

source
theorem abs_lt_of_lt_of_neg_lt {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b : α} (h1 : a < b) (h2 : -a < b) :
abs a < b

source
theorem abs_add_le_abs_add_abs {α : Type u} [decidable_linear_ordered_add_comm_group α] (a b : α) :
abs (a + b) ≤ abs a + abs b

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

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

source
theorem abs_add_three {α : Type u} [decidable_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} [decidable_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 decidable_linear_ordered_add_comm_group.eq_of_abs_sub_nonpos {α : Type u} [decidable_linear_ordered_add_comm_group α] {a b : α} (h : abs (a - b) ≤ 0) :
a = b

source
@[instance]
def nonneg_add_comm_group.to_add_comm_group (α : Type u_1) [s : 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
@[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_decidable_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)) :
decidable_linear_ordered_add_comm_group α

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

Equations
source
@[instance]
def order_dual.ordered_add_comm_monoid {α : Type u} [ordered_add_comm_monoid α] :
ordered_add_comm_monoid (order_dual α)

Equations
source
@[instance]
def order_dual.ordered_cancel_add_comm_monoid {α : Type u} [ordered_cancel_add_comm_monoid α] :
ordered_cancel_add_comm_monoid (order_dual α)

Equations
source
@[instance]
def order_dual.ordered_add_comm_group {α : Type u} [ordered_add_comm_group α] :
ordered_add_comm_group (order_dual α)

Equations
source
@[instance]
def order_dual.decidable_linear_ordered_add_comm_group {α : Type u} [decidable_linear_ordered_add_comm_group α] :
decidable_linear_ordered_add_comm_group (order_dual α)

Equations
source
@[instance]
def multiplicative.preorder {α : Type u} [preorder α] :
preorder (multiplicative α)

Equations
source
@[instance]
def additive.preorder {α : Type u} [preorder α] :
preorder (additive α)

Equations
source
@[instance]
def multiplicative.partial_order {α : Type u} [partial_order α] :
partial_order (multiplicative α)

Equations
source
@[instance]
def additive.partial_order {α : Type u} [partial_order α] :
partial_order (additive α)

Equations
source
@[instance]
def multiplicative.linear_order {α : Type u} [linear_order α] :
linear_order (multiplicative α)

Equations
source
@[instance]
def additive.linear_order {α : Type u} [linear_order α] :
linear_order (additive α)

Equations
source
@[instance]
def multiplicative.decidable_linear_order {α : Type u} [decidable_linear_order α] :
decidable_linear_order (multiplicative α)

Equations
source
@[instance]
def additive.decidable_linear_order {α : Type u} [decidable_linear_order α] :
decidable_linear_order (additive α)

Equations
source
@[instance]
def multiplicative.ordered_comm_monoid {α : Type u} [ordered_add_comm_monoid α] :
ordered_comm_monoid (multiplicative α)

Equations
source
@[instance]
def additive.ordered_add_comm_monoid {α : Type u} [ordered_comm_monoid α] :
ordered_add_comm_monoid (additive α)

Equations
source
@[instance]
def multiplicative.ordered_cancel_comm_monoid {α : Type u} [ordered_cancel_add_comm_monoid α] :
ordered_cancel_comm_monoid (multiplicative α)

Equations
source
@[instance]
def additive.ordered_cancel_add_comm_monoid {α : Type u} [ordered_cancel_comm_monoid α] :
ordered_cancel_add_comm_monoid (additive α)

Equations
source
@[instance]
def multiplicative.ordered_comm_group {α : Type u} [ordered_add_comm_group α] :
ordered_comm_group (multiplicative α)

Equations
source
@[instance]
def additive.ordered_add_comm_group {α : Type u} [ordered_comm_group α] :
ordered_add_comm_group (additive α)

Equations