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.

@[instance]

@[instance]

@[class]
structure ordered_comm_monoid  :
Type u_1Type 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 bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • mul_le_mul_left : ∀ (a b : α), a b∀ (c_1 : α), c_1 * a c_1 * b
  • lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1b < 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
@[class]
structure ordered_add_comm_monoid  :
Type u_1Type 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 bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • add_le_add_left : ∀ (a b : α), a b∀ (c_1 : α), c_1 + a c_1 + b
  • lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1b < 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
theorem mul_le_mul_left' {α : Type u} [ordered_comm_monoid α] {a b : α} (h : a b) (c : α) :
c * a c * b

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

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

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

theorem lt_of_add_lt_add_left {α : Type u} [ordered_add_comm_monoid α] {a b c : α} :
a + b < a + cb < c

theorem lt_of_mul_lt_mul_left' {α : Type u} [ordered_comm_monoid α] {a b c : α} :
a * b < a * cb < c

theorem add_le_add {α : Type u} [ordered_add_comm_monoid α] {a b c d : α} :
a bc da + c b + d

theorem mul_le_mul' {α : Type u} [ordered_comm_monoid α] {a b c d : α} :
a bc da * c b * d

theorem mul_le_mul_three {α : Type u} [ordered_comm_monoid α] {a b c d e f : α} :
a db ec f(a * b) * c (d * e) * f

theorem add_le_add_three {α : Type u} [ordered_add_comm_monoid α] {a b c d e f : α} :
a db ec fa + b + c d + e + f

theorem le_add_of_nonneg_right {α : Type u} [ordered_add_comm_monoid α] {a b : α} :
0 ba a + b

theorem le_mul_of_one_le_right' {α : Type u} [ordered_comm_monoid α] {a b : α} :
1 ba a * b

theorem le_mul_of_one_le_left' {α : Type u} [ordered_comm_monoid α] {a b : α} :
1 ba b * a

theorem le_add_of_nonneg_left {α : Type u} [ordered_add_comm_monoid α] {a b : α} :
0 ba b + a

theorem lt_of_add_lt_add_right {α : Type u} [ordered_add_comm_monoid α] {a b c : α} :
a + b < c + ba < c

theorem lt_of_mul_lt_mul_right' {α : Type u} [ordered_comm_monoid α] {a b c : α} :
a * b < c * ba < c

theorem le_add_of_nonneg_of_le {α : Type u} [ordered_add_comm_monoid α] {a b c : α} :
0 ab cb a + c

theorem le_mul_of_one_le_of_le {α : Type u} [ordered_comm_monoid α] {a b c : α} :
1 ab cb a * c

theorem le_add_of_le_of_nonneg {α : Type u} [ordered_add_comm_monoid α] {a b c : α} :
b c0 ab c + a

theorem le_mul_of_le_of_one_le {α : Type u} [ordered_comm_monoid α] {a b c : α} :
b c1 ab c * a

theorem one_le_mul {α : Type u} [ordered_comm_monoid α] {a b : α} :
1 a1 b1 a * b

theorem add_nonneg {α : Type u} [ordered_add_comm_monoid α] {a b : α} :
0 a0 b0 a + b

theorem one_lt_mul_of_lt_of_le' {α : Type u} [ordered_comm_monoid α] {a b : α} :
1 < a1 b1 < a * b

theorem add_pos_of_pos_of_nonneg {α : Type u} [ordered_add_comm_monoid α] {a b : α} :
0 < a0 b0 < a + b

theorem add_pos_of_nonneg_of_pos {α : Type u} [ordered_add_comm_monoid α] {a b : α} :
0 a0 < b0 < a + b

theorem one_lt_mul_of_le_of_lt' {α : Type u} [ordered_comm_monoid α] {a b : α} :
1 a1 < b1 < a * b

theorem one_lt_mul' {α : Type u} [ordered_comm_monoid α] {a b : α} :
1 < a1 < b1 < a * b

theorem add_pos {α : Type u} [ordered_add_comm_monoid α] {a b : α} :
0 < a0 < b0 < a + b

theorem add_nonpos {α : Type u} [ordered_add_comm_monoid α] {a b : α} :
a 0b 0a + b 0

theorem mul_le_one' {α : Type u} [ordered_comm_monoid α] {a b : α} :
a 1b 1a * b 1

theorem mul_le_of_le_one_of_le' {α : Type u} [ordered_comm_monoid α] {a b c : α} :
a 1b ca * b c

theorem add_le_of_nonpos_of_le' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} :
a 0b ca + b c

theorem add_le_of_le_of_nonpos' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} :
b ca 0b + a c

theorem mul_le_of_le_of_le_one' {α : Type u} [ordered_comm_monoid α] {a b c : α} :
b ca 1b * a c

theorem add_neg_of_neg_of_nonpos' {α : Type u} [ordered_add_comm_monoid α] {a b : α} :
a < 0b 0a + b < 0

theorem mul_lt_one_of_lt_one_of_le_one' {α : Type u} [ordered_comm_monoid α] {a b : α} :
a < 1b 1a * b < 1

theorem mul_lt_one_of_le_one_of_lt_one' {α : Type u} [ordered_comm_monoid α] {a b : α} :
a 1b < 1a * b < 1

theorem add_neg_of_nonpos_of_neg' {α : Type u} [ordered_add_comm_monoid α] {a b : α} :
a 0b < 0a + b < 0

theorem mul_lt_one' {α : Type u} [ordered_comm_monoid α] {a b : α} :
a < 1b < 1a * b < 1

theorem add_neg' {α : Type u} [ordered_add_comm_monoid α] {a b : α} :
a < 0b < 0a + b < 0

theorem lt_mul_of_one_le_of_lt' {α : Type u} [ordered_comm_monoid α] {a b c : α} :
1 ab < cb < a * c

theorem lt_add_of_nonneg_of_lt' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} :
0 ab < cb < a + c

theorem lt_mul_of_lt_of_one_le' {α : Type u} [ordered_comm_monoid α] {a b c : α} :
b < c1 ab < c * a

theorem lt_add_of_lt_of_nonneg' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} :
b < c0 ab < c + a

theorem lt_add_of_pos_of_lt' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} :
0 < ab < cb < a + c

theorem lt_mul_of_one_lt_of_lt' {α : Type u} [ordered_comm_monoid α] {a b c : α} :
1 < ab < cb < a * c

theorem lt_add_of_lt_of_pos' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} :
b < c0 < ab < c + a

theorem lt_mul_of_lt_of_one_lt' {α : Type u} [ordered_comm_monoid α] {a b c : α} :
b < c1 < ab < c * a

theorem add_lt_of_nonpos_of_lt' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} :
a 0b < ca + b < c

theorem mul_lt_of_le_one_of_lt' {α : Type u} [ordered_comm_monoid α] {a b c : α} :
a 1b < ca * b < c

theorem mul_lt_of_lt_of_le_one' {α : Type u} [ordered_comm_monoid α] {a b c : α} :
b < ca 1b * a < c

theorem add_lt_of_lt_of_nonpos' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} :
b < ca 0b + a < c

theorem mul_lt_of_lt_one_of_lt' {α : Type u} [ordered_comm_monoid α] {a b c : α} :
a < 1b < ca * b < c

theorem add_lt_of_neg_of_lt' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} :
a < 0b < ca + b < c

theorem mul_lt_of_lt_of_lt_one' {α : Type u} [ordered_comm_monoid α] {a b c : α} :
b < ca < 1b * a < c

theorem add_lt_of_lt_of_neg' {α : Type u} [ordered_add_comm_monoid α] {a b c : α} :
b < ca < 0b + a < c

theorem add_eq_zero_iff' {α : Type u} [ordered_add_comm_monoid α] {a b : α} :
0 a0 b(a + b = 0 a = 0 b = 0)

theorem mul_eq_one_iff' {α : Type u} [ordered_comm_monoid α] {a b : α} :
1 a1 b(a * b = 1 a = 1 b = 1)

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

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

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

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

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

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

theorem bit0_pos {α : Type u} [ordered_add_comm_monoid α] {a : α} :
0 < a0 < bit0 a

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

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

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

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

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

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

@[instance]

@[instance]

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

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

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

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

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

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

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

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

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

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

Equations
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

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

@[instance]
def with_top.has_one {α : Type u} [has_one α] :

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

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

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

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

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

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

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

@[simp]
theorem with_top.top_ne_one {α : Type u} [has_one α] :

@[simp]
theorem with_top.top_ne_zero {α : Type u} [has_zero α] :

@[simp]
theorem with_top.zero_ne_top {α : Type u} [has_zero α] :

@[simp]
theorem with_top.one_ne_top {α : Type u} [has_one α] :

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

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

theorem with_top.coe_bit0 {α : Type u} [has_add α] {a : α} :

theorem with_top.coe_bit1 {α : Type u} [has_add α] [has_one α] {a : α} :

@[instance]
def with_top.add_monoid {α : Type u} [add_monoid α] :

Equations
def with_top.coe_add_hom {α : Type u} [add_monoid α] :

Coercion from α to with_top α as an add_monoid_hom.

Equations
@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem with_bot.coe_bit0 {α : Type u} [add_semigroup α] {a : α} :

theorem with_bot.coe_bit1 {α : Type u} [add_semigroup α] [has_one α] {a : α} :

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

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

@[class]
structure canonically_ordered_add_monoid  :
Type u_1Type 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 bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • add_le_add_left : ∀ (a b : α), a b∀ (c_1 : α), c_1 + a c_1 + b
  • lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1b < 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
theorem le_iff_exists_add {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :
a b ∃ (c : α), b = a + c

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

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

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

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

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

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

theorem le_add_left {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} :
a ca b + c

theorem le_add_right {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} :
a ba b + c

@[class]
structure canonically_linear_ordered_add_monoid  :
Type u_1Type 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 bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • add_le_add_left : ∀ (a b : α), a b∀ (c_1 : α), c_1 + a c_1 + b
  • lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1b < 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.

@[class]
structure ordered_cancel_add_comm_monoid  :
Type uType 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_1b = c_1
  • add_right_cancel : ∀ (a b c_1 : α), a + b = c_1 + ba = c_1
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • add_le_add_left : ∀ (a b : α), a b∀ (c_1 : α), c_1 + a c_1 + b
  • le_of_add_le_add_left : ∀ (a b c_1 : α), a + b a + c_1b 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
@[class]
structure ordered_cancel_comm_monoid  :
Type uType 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_1b = c_1
  • mul_right_cancel : ∀ (a b c_1 : α), a * b = c_1 * ba = c_1
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • mul_le_mul_left : ∀ (a b : α), a b∀ (c_1 : α), c_1 * a c_1 * b
  • le_of_mul_le_mul_left : ∀ (a b c_1 : α), a * b a * c_1b c_1

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

Instances
theorem le_of_mul_le_mul_left' {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :
a * b a * cb c

theorem le_of_add_le_add_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :
a + b a + cb c

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

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

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

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

theorem mul_lt_mul''' {α : Type u} [ordered_cancel_comm_monoid α] {a b c d : α} :
a < bc < da * c < b * d

theorem add_lt_add {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c d : α} :
a < bc < da + c < b + d

theorem mul_lt_mul_of_le_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c d : α} :
a bc < da * c < b * d

theorem add_lt_add_of_le_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c d : α} :
a bc < da + c < b + d

theorem add_lt_add_of_lt_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c d : α} :
a < bc da + c < b + d

theorem mul_lt_mul_of_lt_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c d : α} :
a < bc da * c < b * d

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

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

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

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

theorem le_of_mul_le_mul_right' {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :
a * b c * ba c

theorem le_of_add_le_add_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :
a + b c + ba c

theorem mul_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :
a < 1b < 1a * b < 1

theorem add_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :
a < 0b < 0a + b < 0

theorem add_neg_of_neg_of_nonpos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :
a < 0b 0a + b < 0

theorem mul_lt_one_of_lt_one_of_le_one {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :
a < 1b 1a * b < 1

theorem mul_lt_one_of_le_one_of_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :
a 1b < 1a * b < 1

theorem add_neg_of_nonpos_of_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :
a 0b < 0a + b < 0

theorem lt_add_of_pos_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :
0 < ab cb < a + c

theorem lt_mul_of_one_lt_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :
1 < ab cb < a * c

theorem lt_add_of_le_of_pos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :
b c0 < ab < c + a

theorem lt_mul_of_le_of_one_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :
b c1 < ab < c * a

theorem add_le_of_nonpos_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :
a 0b ca + b c

theorem mul_le_of_le_one_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :
a 1b ca * b c

theorem mul_le_of_le_of_le_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :
b ca 1b * a c

theorem add_le_of_le_of_nonpos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :
b ca 0b + a c

theorem mul_lt_of_lt_one_of_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :
a < 1b ca * b < c

theorem add_lt_of_neg_of_le {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :
a < 0b ca + b < c

theorem add_lt_of_le_of_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :
b ca < 0b + a < c

theorem mul_lt_of_le_of_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :
b ca < 1b * a < c

theorem lt_mul_of_one_le_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :
1 ab < cb < a * c

theorem lt_add_of_nonneg_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :
0 ab < cb < a + c

theorem lt_mul_of_lt_of_one_le {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :
b < c1 ab < c * a

theorem lt_add_of_lt_of_nonneg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :
b < c0 ab < c + a

theorem lt_mul_of_one_lt_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :
1 < ab < cb < a * c

theorem lt_add_of_pos_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :
0 < ab < cb < a + c

theorem lt_mul_of_lt_of_one_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :
b < c1 < ab < c * a

theorem lt_add_of_lt_of_pos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :
b < c0 < ab < c + a

theorem mul_lt_of_le_one_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :
a 1b < ca * b < c

theorem add_lt_of_nonpos_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :
a 0b < ca + b < c

theorem add_lt_of_lt_of_nonpos {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :
b < ca 0b + a < c

theorem mul_lt_of_lt_of_le_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :
b < ca 1b * a < c

theorem add_lt_of_neg_of_lt {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :
a < 0b < ca + b < c

theorem mul_lt_of_lt_one_of_lt {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :
a < 1b < ca * b < c

theorem mul_lt_of_lt_of_lt_one {α : Type u} [ordered_cancel_comm_monoid α] {a b c : α} :
b < ca < 1b * a < c

theorem add_lt_of_lt_of_neg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : α} :
b < ca < 0b + a < c

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem mul_eq_one_iff_eq_one_of_one_le {α : Type u} [ordered_cancel_comm_monoid α] {a b : α} :
1 a1 b(a * b = 1 a = 1 b = 1)

theorem add_eq_zero_iff_eq_zero_of_nonneg {α : Type u} [ordered_cancel_add_comm_monoid α] {a b : α} :
0 a0 b(a + b = 0 a = 0 b = 0)

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

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

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

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

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)

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)

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)

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)

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

theorem with_bot.add_lt_add_iff_left {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_bot α} :
< a(a + c < a + b c < b)

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

theorem with_bot.add_lt_add_iff_right {α : Type u} [ordered_cancel_add_comm_monoid α] {a b c : with_bot α} :
< a(c + a < b + a c < b)

@[class]
structure ordered_add_comm_group  :
Type uType 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 bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • add_le_add_left : ∀ (a b : α), a b∀ (c_1 : α), c_1 + a c_1 + b

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

Instances
@[instance]

@[class]
structure ordered_comm_group  :
Type uType 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 bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • mul_le_mul_left : ∀ (a b : α), a b∀ (c_1 : α), c_1 * a c_1 * b

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

Instances
@[instance]

@[instance]

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

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

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

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

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

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

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

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

theorem inv_le_inv' {α : Type u} [ordered_comm_group α] {a b : α} :
a bb⁻¹ a⁻¹

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

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

theorem one_le_of_inv_le_one {α : Type u} [ordered_comm_group α] {a : α} :
a⁻¹ 11 a

theorem nonneg_of_neg_nonpos {α : Type u} [ordered_add_comm_group α] {a : α} :
-a 00 a

theorem inv_le_one_of_one_le {α : Type u} [ordered_comm_group α] {a : α} :
1 aa⁻¹ 1

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

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

theorem nonpos_of_neg_nonneg {α : Type u} [ordered_add_comm_group α] {a : α} :
0 -aa 0

theorem one_le_inv_of_le_one {α : Type u} [ordered_comm_group α] {a : α} :
a 11 a⁻¹

theorem neg_nonneg_of_nonpos {α : Type u} [ordered_add_comm_group α] {a : α} :
a 00 -a

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

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

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

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

theorem pos_of_neg_neg {α : Type u} [ordered_add_comm_group α] {a : α} :
-a < 00 < a

theorem one_lt_of_inv_inv {α : Type u} [ordered_comm_group α] {a : α} :
a⁻¹ < 11 < a

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

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

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

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

theorem one_lt_inv_of_inv {α : Type u} [ordered_comm_group α] {a : α} :
a < 11 < a⁻¹

theorem neg_pos_of_neg {α : Type u} [ordered_add_comm_group α] {a : α} :
a < 00 < -a

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

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

theorem inv_le_of_inv_le {α : Type u} [ordered_comm_group α] {a b : α} :
a⁻¹ bb⁻¹ a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem inv_le_self {α : Type u} [ordered_comm_group α] {a : α} :
1 aa⁻¹ a

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

theorem self_le_inv {α : Type u} [ordered_comm_group α] {a : α} :
a 1a a⁻¹

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem sub_le_sub {α : Type u} [ordered_add_comm_group α] {a b c d : α} :
a bc da - d b - c

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem sub_lt_sub {α : Type u} [ordered_add_comm_group α] {a b c d : α} :
a < bc < da - d < b - c

theorem sub_lt_sub_of_le_of_lt {α : Type u} [ordered_add_comm_group α] {a b c d : α} :
a bc < da - d < b - c

theorem sub_lt_sub_of_lt_of_le {α : Type u} [ordered_add_comm_group α] {a b c d : α} :
a < bc da - d < b - c

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

def ordered_comm_group.mk' {α : Type u} [comm_group α] [partial_order α] :
(∀ (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
def ordered_add_comm_group.mk' {α : Type u} [add_comm_group α] [partial_order α] :
(∀ (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.

@[class]
structure decidable_linear_ordered_cancel_add_comm_monoid  :
Type uType 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_1b = c_1
  • add_right_cancel : ∀ (a b c_1 : α), a + b = c_1 + ba = c_1
  • le : α → α → Prop
  • lt : α → α → Prop
  • le_refl : ∀ (a : α), a a
  • le_trans : ∀ (a b c_1 : α), a bb c_1a c_1
  • lt_iff_le_not_le : (∀ (a b : α), a < b a b ¬b a) . "order_laws_tac"
  • le_antisymm : ∀ (a b : α), a bb aa = b
  • add_le_add_left : ∀ (a b : α), a b∀ (c_1 : α), c_1 + a c_1 + b
  • le_of_add_le_add_left : ∀ (a b c_1 : α), a + b a + c_1b 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

Some lemmas about types that have an ordering and a binary operation, with no rules relating them.

theorem fn_min_mul_fn_max {α : Type u} {β : Type u_1} [decidable_linear_order α] [comm_semigroup β] (f : α → β) (n m : α) :
(f (min n m)) * f (max n m) = (f n) * f m

theorem fn_min_add_fn_max {α : Type u} {β : Type u_1} [decidable_linear_order α] [add_comm_semigroup β] (f : α → β) (n m : α) :
f (min n m) + f (max n m) = f n + f m

theorem min_add_max {α : Type u}