# mathlibdocumentation

algebra.ordered_monoid

# Ordered monoids #

This file develops the basics of ordered monoids.

## 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]
def ordered_comm_monoid.to_comm_monoid (α : Type u_1) [self : ordered_comm_monoid α] :
@[instance]
def ordered_comm_monoid.to_partial_order (α : Type u_1) [self : ordered_comm_monoid α] :
@[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
• npow : α → α
• npow_zero' : (∀ (x : α), . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• 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
@[instance]
@[instance]
@[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
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• 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
@[class]
structure has_exists_mul_of_le (α : Type u)  :
Prop
• exists_mul_of_le : ∀ {a b : α}, a b(∃ (c : α), b = a * c)

An `ordered_comm_monoid` with one-sided 'division' in the sense that if `a ≤ b`, there is some `c` for which `a * c = b`. This is a weaker version of the condition on canonical orderings defined by `canonically_ordered_monoid`.

Instances
@[class]
structure has_exists_add_of_le (α : Type u)  :
Prop
• exists_add_of_le : ∀ {a b : α}, a b(∃ (c : α), b = a + c)

An `ordered_add_comm_monoid` with one-sided 'subtraction' in the sense that if `a ≤ b`, then there is some `c` for which `a + c = b`. This is a weaker version of the condition on canonical orderings defined by `canonically_ordered_add_monoid`.

Instances
@[class]
structure linear_ordered_add_comm_monoid (α : Type u_1) :
Type u_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
• le_total : ∀ (a b : α), a b b a
• decidable_le :
• decidable_eq :
• decidable_lt :
• 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
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• add_comm : ∀ (a b : α), a + b = b + a
• 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

A linearly ordered additive commutative monoid.

Instances
@[class]
structure linear_ordered_comm_monoid (α : Type u_1) :
Type u_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
• le_total : ∀ (a b : α), a b b a
• decidable_le :
• decidable_eq :
• decidable_lt :
• 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
• npow : α → α
• npow_zero' : (∀ (x : α), . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• mul_comm : ∀ (a b : α), a * b = b * a
• 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

A linearly ordered commutative monoid.

Instances
@[instance]
@[class]
structure linear_ordered_comm_monoid_with_zero (α : Type u_1) :
Type u_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
• le_total : ∀ (a b : α), a b b a
• decidable_le :
• decidable_eq :
• decidable_lt :
• 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
• npow : α → α
• npow_zero' : (∀ (x : α), . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• mul_comm : ∀ (a b : α), a * b = b * a
• 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
• zero : α
• zero_mul : ∀ (a : α), 0 * a = 0
• mul_zero : ∀ (a : α), a * 0 = 0
• zero_le_one : 0 1

A linearly ordered commutative monoid with a zero element.

Instances
@[instance]
@[instance]
@[instance]
@[class]
structure linear_ordered_add_comm_monoid_with_top (α : Type u_1) :
Type u_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
• le_total : ∀ (a b : α), a b b a
• decidable_le :
• decidable_eq :
• decidable_lt :
• 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
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• add_comm : ∀ (a b : α), a + b = b + a
• 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
• top : α
• le_top : ∀ (a : α), a
• top_add' : ∀ (x : α), + x =

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

Instances
@[simp]
theorem top_add {α : Type u} (a : α) :
@[simp]
theorem add_top {α : Type u} (a : α) :
theorem mul_le_mul_left' {α : Type u} {a b : α} (h : a b) (c : α) :
c * a c * b
theorem add_le_add_left {α : Type u} {a b : α} (h : a b) (c : α) :
c + a c + b
theorem add_le_add_right {α : Type u} {a b : α} (h : a b) (c : α) :
a + c b + c
theorem mul_le_mul_right' {α : Type u} {a b : α} (h : a b) (c : α) :
a * c b * c
theorem mul_lt_of_mul_lt_left {α : Type u} {a b c d : α} (h : a * b < c) (hle : d b) :
a * d < c
theorem add_lt_of_add_lt_left {α : Type u} {a b c d : α} (h : a + b < c) (hle : d b) :
a + d < c
theorem mul_lt_of_mul_lt_right {α : Type u} {a b c d : α} (h : a * b < c) (hle : d a) :
d * b < c
theorem add_lt_of_add_lt_right {α : Type u} {a b c d : α} (h : a + b < c) (hle : d a) :
d + b < c
theorem add_le_of_add_le_left {α : Type u} {a b c d : α} (h : a + b c) (hle : d b) :
a + d c
theorem mul_le_of_mul_le_left {α : Type u} {a b c d : α} (h : a * b c) (hle : d b) :
a * d c
theorem mul_le_of_mul_le_right {α : Type u} {a b c d : α} (h : a * b c) (hle : d a) :
d * b c
theorem add_le_of_add_le_right {α : Type u} {a b c d : α} (h : a + b c) (hle : d a) :
d + b c
theorem lt_add_of_lt_add_left {α : Type u} {a b c d : α} (h : a < b + c) (hle : c d) :
a < b + d
theorem lt_mul_of_lt_mul_left {α : Type u} {a b c d : α} (h : a < b * c) (hle : c d) :
a < b * d
theorem lt_add_of_lt_add_right {α : Type u} {a b c d : α} (h : a < b + c) (hle : b d) :
a < d + c
theorem lt_mul_of_lt_mul_right {α : Type u} {a b c d : α} (h : a < b * c) (hle : b d) :
a < d * c
theorem le_add_of_le_add_left {α : Type u} {a b c d : α} (h : a b + c) (hle : c d) :
a b + d
theorem le_mul_of_le_mul_left {α : Type u} {a b c d : α} (h : a b * c) (hle : c d) :
a b * d
theorem le_mul_of_le_mul_right {α : Type u} {a b c d : α} (h : a b * c) (hle : b d) :
a d * c
theorem le_add_of_le_add_right {α : Type u} {a b c d : α} (h : a b + c) (hle : b d) :
a d + c
theorem lt_of_add_lt_add_left {α : Type u} {a b c : α} :
a + b < a + cb < c
theorem lt_of_mul_lt_mul_left' {α : Type u} {a b c : α} :
a * b < a * cb < c
theorem lt_of_add_lt_add_right {α : Type u} {a b c : α} (h : a + b < c + b) :
a < c
theorem lt_of_mul_lt_mul_right' {α : Type u} {a b c : α} (h : a * b < c * b) :
a < c
theorem add_le_add {α : Type u} {a b c d : α} (h₁ : a b) (h₂ : c d) :
a + c b + d
theorem mul_le_mul' {α : Type u} {a b c d : α} (h₁ : a b) (h₂ : c d) :
a * c b * d
theorem mul_le_mul_three {α : Type u} {a b c d e f : α} (h₁ : a d) (h₂ : b e) (h₃ : c f) :
(a * b) * c (d * e) * f
theorem add_le_add_three {α : Type u} {a b c d e f : α} (h₁ : a d) (h₂ : b e) (h₃ : c f) :
a + b + c d + e + f
theorem le_add_of_nonneg_right {α : Type u} {a b : α} (h : 0 b) :
a a + b
theorem le_mul_of_one_le_right' {α : Type u} {a b : α} (h : 1 b) :
a a * b
theorem le_mul_of_one_le_left' {α : Type u} {a b : α} (h : 1 b) :
a b * a
theorem le_add_of_nonneg_left {α : Type u} {a b : α} (h : 0 b) :
a b + a
theorem mul_le_of_le_one_right' {α : Type u} {a b : α} (h : b 1) :
a * b a
theorem add_le_of_nonpos_right {α : Type u} {a b : α} (h : b 0) :
a + b a
theorem add_le_of_nonpos_left {α : Type u} {a b : α} (h : b 0) :
b + a a
theorem mul_le_of_le_one_left' {α : Type u} {a b : α} (h : b 1) :
b * a a
theorem lt_of_mul_lt_of_one_le_left {α : Type u} {a b c : α} (h : a * b < c) (hle : 1 b) :
a < c
theorem lt_of_add_lt_of_nonneg_left {α : Type u} {a b c : α} (h : a + b < c) (hle : 0 b) :
a < c
theorem lt_of_mul_lt_of_one_le_right {α : Type u} {a b c : α} (h : a * b < c) (hle : 1 a) :
b < c
theorem lt_of_add_lt_of_nonneg_right {α : Type u} {a b c : α} (h : a + b < c) (hle : 0 a) :
b < c
theorem le_of_mul_le_of_one_le_left {α : Type u} {a b c : α} (h : a * b c) (hle : 1 b) :
a c
theorem le_of_add_le_of_nonneg_left {α : Type u} {a b c : α} (h : a + b c) (hle : 0 b) :
a c
theorem le_of_mul_le_of_one_le_right {α : Type u} {a b c : α} (h : a * b c) (hle : 1 a) :
b c
theorem le_of_add_le_of_nonneg_right {α : Type u} {a b c : α} (h : a + b c) (hle : 0 a) :
b c
theorem lt_of_lt_add_of_nonpos_left {α : Type u} {a b c : α} (h : a < b + c) (hle : c 0) :
a < b
theorem lt_of_lt_mul_of_le_one_left {α : Type u} {a b c : α} (h : a < b * c) (hle : c 1) :
a < b
theorem lt_of_lt_add_of_nonpos_right {α : Type u} {a b c : α} (h : a < b + c) (hle : b 0) :
a < c
theorem lt_of_lt_mul_of_le_one_right {α : Type u} {a b c : α} (h : a < b * c) (hle : b 1) :
a < c
theorem le_of_le_add_of_nonpos_left {α : Type u} {a b c : α} (h : a b + c) (hle : c 0) :
a b
theorem le_of_le_mul_of_le_one_left {α : Type u} {a b c : α} (h : a b * c) (hle : c 1) :
a b
theorem le_of_le_mul_of_le_one_right {α : Type u} {a b c : α} (h : a b * c) (hle : b 1) :
a c
theorem le_of_le_add_of_nonpos_right {α : Type u} {a b c : α} (h : a b + c) (hle : b 0) :
a c
theorem le_add_of_nonneg_of_le {α : Type u} {a b c : α} (ha : 0 a) (hbc : b c) :
b a + c
theorem le_mul_of_one_le_of_le {α : Type u} {a b c : α} (ha : 1 a) (hbc : b c) :
b a * c
theorem le_add_of_le_of_nonneg {α : Type u} {a b c : α} (hbc : b c) (ha : 0 a) :
b c + a
theorem le_mul_of_le_of_one_le {α : Type u} {a b c : α} (hbc : b c) (ha : 1 a) :
b c * a
theorem one_le_mul {α : Type u} {a b : α} (ha : 1 a) (hb : 1 b) :
1 a * b
theorem add_nonneg {α : Type u} {a b : α} (ha : 0 a) (hb : 0 b) :
0 a + b
theorem one_lt_mul_of_lt_of_le' {α : Type u} {a b : α} (ha : 1 < a) (hb : 1 b) :
1 < a * b
theorem add_pos_of_pos_of_nonneg {α : Type u} {a b : α} (ha : 0 < a) (hb : 0 b) :
0 < a + b
theorem add_pos_of_nonneg_of_pos {α : Type u} {a b : α} (ha : 0 a) (hb : 0 < b) :
0 < a + b
theorem one_lt_mul_of_le_of_lt' {α : Type u} {a b : α} (ha : 1 a) (hb : 1 < b) :
1 < a * b
theorem one_lt_mul' {α : Type u} {a b : α} (ha : 1 < a) (hb : 1 < b) :
1 < a * b
theorem add_pos {α : Type u} {a b : α} (ha : 0 < a) (hb : 0 < b) :
0 < a + b
theorem add_nonpos {α : Type u} {a b : α} (ha : a 0) (hb : b 0) :
a + b 0
theorem mul_le_one' {α : Type u} {a b : α} (ha : a 1) (hb : b 1) :
a * b 1
theorem mul_le_of_le_one_of_le' {α : Type u} {a b c : α} (ha : a 1) (hbc : b c) :
a * b c
theorem add_le_of_nonpos_of_le' {α : Type u} {a b c : α} (ha : a 0) (hbc : b c) :
a + b c
theorem add_le_of_le_of_nonpos' {α : Type u} {a b c : α} (hbc : b c) (ha : a 0) :
b + a c
theorem mul_le_of_le_of_le_one' {α : Type u} {a b c : α} (hbc : b c) (ha : a 1) :
b * a c
theorem add_neg_of_neg_of_nonpos' {α : Type u} {a b : α} (ha : a < 0) (hb : b 0) :
a + b < 0
theorem mul_lt_one_of_lt_one_of_le_one' {α : Type u} {a b : α} (ha : a < 1) (hb : b 1) :
a * b < 1
theorem mul_lt_one_of_le_one_of_lt_one' {α : Type u} {a b : α} (ha : a 1) (hb : b < 1) :
a * b < 1
theorem add_neg_of_nonpos_of_neg' {α : Type u} {a b : α} (ha : a 0) (hb : b < 0) :
a + b < 0
theorem mul_lt_one' {α : Type u} {a b : α} (ha : a < 1) (hb : b < 1) :
a * b < 1
theorem add_neg' {α : Type u} {a b : α} (ha : a < 0) (hb : b < 0) :
a + b < 0
theorem lt_mul_of_one_le_of_lt' {α : Type u} {a b c : α} (ha : 1 a) (hbc : b < c) :
b < a * c
theorem lt_add_of_nonneg_of_lt' {α : Type u} {a b c : α} (ha : 0 a) (hbc : b < c) :
b < a + c
theorem lt_mul_of_lt_of_one_le' {α : Type u} {a b c : α} (hbc : b < c) (ha : 1 a) :
b < c * a
theorem lt_add_of_lt_of_nonneg' {α : Type u} {a b c : α} (hbc : b < c) (ha : 0 a) :
b < c + a
theorem lt_add_of_pos_of_lt' {α : Type u} {a b c : α} (ha : 0 < a) (hbc : b < c) :
b < a + c
theorem lt_mul_of_one_lt_of_lt' {α : Type u} {a b c : α} (ha : 1 < a) (hbc : b < c) :
b < a * c
theorem lt_add_of_lt_of_pos' {α : Type u} {a b c : α} (hbc : b < c) (ha : 0 < a) :
b < c + a
theorem lt_mul_of_lt_of_one_lt' {α : Type u} {a b c : α} (hbc : b < c) (ha : 1 < a) :
b < c * a
theorem add_lt_of_nonpos_of_lt' {α : Type u} {a b c : α} (ha : a 0) (hbc : b < c) :
a + b < c
theorem mul_lt_of_le_one_of_lt' {α : Type u} {a b c : α} (ha : a 1) (hbc : b < c) :
a * b < c
theorem mul_lt_of_lt_of_le_one' {α : Type u} {a b c : α} (hbc : b < c) (ha : a 1) :
b * a < c
theorem add_lt_of_lt_of_nonpos' {α : Type u} {a b c : α} (hbc : b < c) (ha : a 0) :
b + a < c
theorem mul_lt_of_lt_one_of_lt' {α : Type u} {a b c : α} (ha : a < 1) (hbc : b < c) :
a * b < c
theorem add_lt_of_neg_of_lt' {α : Type u} {a b c : α} (ha : a < 0) (hbc : b < c) :
a + b < c
theorem mul_lt_of_lt_of_lt_one' {α : Type u} {a b c : α} (hbc : b < c) (ha : a < 1) :
b * a < c
theorem add_lt_of_lt_of_neg' {α : Type u} {a b c : α} (hbc : b < c) (ha : a < 0) :
b + a < c
theorem add_eq_zero_iff' {α : Type u} {a b : α} (ha : 0 a) (hb : 0 b) :
a + b = 0 a = 0 b = 0
theorem mul_eq_one_iff' {α : Type u} {a b : α} (ha : 1 a) (hb : 1 b) :
a * b = 1 a = 1 b = 1
def function.injective.ordered_comm_monoid {α : Type u} {β : Type u_1} [has_one β] [has_mul β] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

Pullback an `ordered_comm_monoid` under an injective map.

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

Pullback an `ordered_add_comm_monoid` under an injective map.

theorem monotone.mul' {α : Type u} {β : Type u_1} [preorder β] {f g : β → α} (hf : monotone f) (hg : monotone g) :
monotone (λ (x : β), (f x) * g x)
theorem monotone.add {α : Type u} {β : Type u_1} [preorder β] {f g : β → α} (hf : monotone f) (hg : monotone g) :
monotone (λ (x : β), f x + g x)
theorem monotone.add_const {α : Type u} {β : Type u_1} [preorder β] {f : β → α} (hf : monotone f) (a : α) :
monotone (λ (x : β), f x + a)
theorem monotone.mul_const' {α : Type u} {β : Type u_1} [preorder β] {f : β → α} (hf : monotone f) (a : α) :
monotone (λ (x : β), (f x) * a)
theorem monotone.const_add {α : Type u} {β : Type u_1} [preorder β] {f : β → α} (hf : monotone f) (a : α) :
monotone (λ (x : β), a + f x)
theorem monotone.const_mul' {α : Type u} {β : Type u_1} [preorder β] {f : β → α} (hf : monotone f) (a : α) :
monotone (λ (x : β), a * f x)
def function.injective.linear_ordered_comm_monoid {α : Type u} {β : Type u_1} [has_one β] [has_mul β] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

Pullback a `linear_ordered_comm_monoid` under an injective map.

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

Pullback an `ordered_add_comm_monoid` under an injective map.

theorem bit0_pos {α : Type u} {a : α} (h : 0 < a) :
0 < bit0 a
@[protected, instance]
def add_units.preorder {α : Type u} [add_monoid α] [preorder α] :
@[protected, instance]
def units.preorder {α : Type u} [monoid α] [preorder α] :
Equations
@[simp, norm_cast]
theorem add_units.coe_le_coe {α : Type u} [add_monoid α] [preorder α] {a b : add_units α} :
a b a b
@[simp, norm_cast]
theorem units.coe_le_coe {α : Type u} [monoid α] [preorder α] {a b : units α} :
a b a b
@[simp, norm_cast]
theorem add_units.coe_lt_coe {α : Type u} [add_monoid α] [preorder α] {a b : add_units α} :
a < b a < b
@[simp, norm_cast]
theorem units.coe_lt_coe {α : Type u} [monoid α] [preorder α] {a b : units α} :
a < b a < b
@[protected, instance]
def add_units.partial_order {α : Type u} [add_monoid α]  :
@[protected, instance]
def units.partial_order {α : Type u} [monoid α]  :
Equations
@[protected, instance]
def units.linear_order {α : Type u} [monoid α] [linear_order α] :
Equations
@[protected, instance]
def add_units.linear_order {α : Type u} [add_monoid α] [linear_order α] :
@[simp, norm_cast]
theorem add_units.max_coe {α : Type u} [add_monoid α] [linear_order α] {a b : add_units α} :
(max a b) = max a b
@[simp, norm_cast]
theorem units.max_coe {α : Type u} [monoid α] [linear_order α] {a b : units α} :
(max a b) = max a b
@[simp, norm_cast]
theorem units.min_coe {α : Type u} [monoid α] [linear_order α] {a b : units α} :
(min a b) = min a b
@[simp, norm_cast]
theorem add_units.min_coe {α : Type u} [add_monoid α] [linear_order α] {a b : add_units α} :
(min a b) = min a b
@[protected, instance]
def with_zero.preorder {α : Type u} [preorder α] :
Equations
@[protected, instance]
def with_zero.partial_order {α : Type u}  :
Equations
@[protected, instance]
def with_zero.order_bot {α : Type u}  :
Equations
theorem with_zero.zero_le {α : Type u} (a : with_zero α) :
0 a
theorem with_zero.zero_lt_coe {α : Type u} (a : α) :
0 < a
@[simp, norm_cast]
theorem with_zero.coe_lt_coe {α : Type u} {a b : α} :
a < b a < b
@[simp, norm_cast]
theorem with_zero.coe_le_coe {α : Type u} {a b : α} :
a b a b
@[protected, instance]
def with_zero.lattice {α : Type u} [lattice α] :
Equations
@[protected, instance]
def with_zero.linear_order {α : Type u} [linear_order α] :
Equations
theorem with_zero.mul_le_mul_left {α : Type u} (a b : with_zero α) :
a b∀ (c : , c * a c * b
theorem with_zero.lt_of_mul_lt_mul_left {α : Type u} (a b c : with_zero α) :
a * b < a * cb < c
@[protected, instance]
def with_zero.ordered_comm_monoid {α : Type u}  :
Equations
def with_zero.ordered_add_comm_monoid {α : Type u} (zero_le : ∀ (a : α), 0 a) :

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

Equations
@[protected, instance]
def with_top.has_one {α : Type u} [has_one α] :
Equations
@[protected, instance]
def with_top.has_zero {α : Type u} [has_zero α] :
@[simp, norm_cast]
theorem with_top.coe_one {α : Type u} [has_one α] :
1 = 1
@[simp, norm_cast]
theorem with_top.coe_zero {α : Type u} [has_zero α] :
0 = 0
@[simp, norm_cast]
theorem with_top.coe_eq_zero {α : Type u} [has_zero α] {a : α} :
a = 0 a = 0
@[simp, norm_cast]
theorem with_top.coe_eq_one {α : Type u} [has_one α] {a : α} :
a = 1 a = 1
@[simp, norm_cast]
theorem with_top.zero_eq_coe {α : Type u} [has_zero α] {a : α} :
0 = a a = 0
@[simp, norm_cast]
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 α] :
@[protected, instance]
def with_top.has_add {α : Type u} [has_add α] :
Equations
@[protected, instance]
def with_top.add_semigroup {α : Type u}  :
Equations
@[norm_cast]
theorem with_top.coe_add {α : Type u} [has_add α] {a b : α} :
(a + b) = a + b
@[norm_cast]
theorem with_top.coe_bit0 {α : Type u} [has_add α] {a : α} :
(bit0 a) =
@[norm_cast]
theorem with_top.coe_bit1 {α : Type u} [has_add α] [has_one α] {a : α} :
(bit1 a) =
@[simp]
theorem with_top.add_top {α : Type u} [has_add α] {a : with_top α} :
@[simp]
theorem with_top.top_add {α : Type u} [has_add α] {a : with_top α} :
theorem with_top.add_eq_top {α : Type u} [has_add α] {a b : with_top α} :
a + b = a = b =
theorem with_top.add_lt_top {α : Type u} [has_add α] {a b : with_top α} :
a + b < a < b <
theorem with_top.add_eq_coe {α : Type u} [has_add α] {a b : with_top α} {c : α} :
a + b = c ∃ (a' b' : α), a' = a b' = b a' + b' = c
@[protected, instance]
def with_top.add_comm_semigroup {α : Type u}  :
Equations
@[protected, instance]
def with_top.add_monoid {α : Type u} [add_monoid α] :
Equations
@[protected, instance]
def with_top.add_comm_monoid {α : Type u}  :
Equations
@[protected, instance]
def with_top.ordered_add_comm_monoid {α : Type u}  :
Equations
@[protected, instance]
Equations
def with_top.coe_add_hom {α : Type u} [add_monoid α] :
α →+

Coercion from `α` to `with_top α` as an `add_monoid_hom`.

Equations
@[simp]
theorem with_top.coe_coe_add_hom {α : Type u} [add_monoid α] :
@[simp]
theorem with_top.zero_lt_top {α : Type u}  :
0 <
@[simp, norm_cast]
theorem with_top.zero_lt_coe {α : Type u} (a : α) :
0 < a 0 < a
@[protected, instance]
def with_bot.has_zero {α : Type u} [has_zero α] :
Equations
@[protected, instance]
def with_bot.has_one {α : Type u} [has_one α] :
Equations
@[protected, instance]
def with_bot.add_semigroup {α : Type u}  :
Equations
@[protected, instance]
def with_bot.add_comm_semigroup {α : Type u}  :
Equations
@[protected, instance]
def with_bot.add_monoid {α : Type u} [add_monoid α] :
Equations
@[protected, instance]
def with_bot.add_comm_monoid {α : Type u}  :
Equations
@[protected, instance]
def with_bot.ordered_add_comm_monoid {α : Type u}  :
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} (a b : α) :
(a + b) = a + b
theorem with_bot.coe_bit0 {α : Type u} {a : α} :
(bit0 a) =
theorem with_bot.coe_bit1 {α : Type u} [has_one α] {a : α} :
(bit1 a) =
@[simp]
theorem with_bot.bot_add {α : Type u} (a : with_bot α) :
@[simp]
theorem with_bot.add_bot {α : Type u} (a : with_bot α) :
@[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
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• 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 subtractibility 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 nontrivial `ordered_add_comm_group`s.

Instances
@[instance]
@[class]
structure canonically_ordered_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
• npow : α → α
• npow_zero' : (∀ (x : α), . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• 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
• bot : α
• bot_le : ∀ (a : α), a
• le_iff_exists_mul : ∀ (a b : α), a b ∃ (c_1 : α), b = a * c_1

A canonically ordered monoid is an ordered commutative monoid in which the ordering coincides with the divisibility relation, which is to say, `a ≤ b` iff there exists `c` with `b = a * c`. Example seem rare; it seems more likely that the `order_dual` of a naturally-occurring lattice satisfies this than the lattice itself (for example, dual of the lattice of ideals of a PID or Dedekind domain satisfy this; collections of all things ≤ 1 seem to be more natural that collections of all things ≥ 1).

Instances
theorem le_iff_exists_add {α : Type u} {a b : α} :
a b ∃ (c : α), b = a + c
theorem le_iff_exists_mul {α : Type u} {a b : α} :
a b ∃ (c : α), b = a * c
theorem self_le_mul_right {α : Type u} (a b : α) :
a a * b
theorem self_le_add_right {α : Type u} (a b : α) :
a a + b
theorem self_le_add_left {α : Type u} (a b : α) :
a b + a
theorem self_le_mul_left {α : Type u} (a b : α) :
a b * a
@[simp]
theorem one_le {α : Type u} (a : α) :
1 a
@[simp]
theorem zero_le {α : Type u} (a : α) :
0 a
@[simp]
theorem bot_eq_one {α : Type u}  :
= 1
@[simp]
theorem bot_eq_zero {α : Type u}  :
= 0
@[simp]
theorem mul_eq_one_iff {α : Type u} {a b : α} :
a * b = 1 a = 1 b = 1
@[simp]
theorem add_eq_zero_iff {α : Type u} {a b : α} :
a + b = 0 a = 0 b = 0
@[simp]
theorem le_one_iff_eq_one {α : Type u} {a : α} :
a 1 a = 1
@[simp]
theorem nonpos_iff_eq_zero {α : Type u} {a : α} :
a 0 a = 0
theorem one_lt_iff_ne_one {α : Type u} {a : α} :
1 < a a 1
theorem pos_iff_ne_zero {α : Type u} {a : α} :
0 < a a 0
theorem exists_pos_mul_of_lt {α : Type u} {a b : α} (h : a < b) :
∃ (c : α) (H : c > 1), a * c = b
theorem exists_pos_add_of_lt {α : Type u} {a b : α} (h : a < b) :
∃ (c : α) (H : c > 0), a + c = b
theorem le_add_left {α : Type u} {a b c : α} (h : a c) :
a b + c
theorem le_mul_left {α : Type u} {a b c : α} (h : a c) :
a b * c
theorem le_add_right {α : Type u} {a b c : α} (h : a b) :
a b + c
theorem le_mul_right {α : Type u} {a b c : α} (h : a b) :
a b * c
@[protected, instance]

Adding a new zero to a canonically ordered additive monoid produces another one.

Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
theorem pos_of_gt {M : Type u_1} {n m : M} (h : n < m) :
0 < m
@[instance]
@[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
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• 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_eq :
• decidable_lt :

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

Instances
@[class]
structure canonically_linear_ordered_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
• npow : α → α
• npow_zero' : (∀ (x : α), . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• 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
• bot : α
• bot_le : ∀ (a : α), a
• le_iff_exists_mul : ∀ (a b : α), a b ∃ (c_1 : α), b = a * c_1
• le_total : ∀ (a b : α), a b b a
• decidable_le :
• decidable_eq :
• decidable_lt :

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

@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem min_add_distrib {α : Type u} (a b c : α) :
min a (b + c) = min a (min a b + min a c)
theorem min_mul_distrib {α : Type u} (a b c : α) :
min a (b * c) = min a ((min a b) * min a c)
theorem min_mul_distrib' {α : Type u} (a b c : α) :
min (a * b) c = min ((min a c) * min b c) c
theorem min_add_distrib' {α : Type u} (a b c : α) :
min (a + b) c = min (min a c + min b c) c
@[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)
• add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1b = c_1
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• 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
• 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 monotone.

Instances
@[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
• mul_left_cancel : ∀ (a b c_1 : α), a * b = a * c_1b = c_1
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• 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
• 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 monotone.

Instances
theorem le_of_mul_le_mul_left' {α : Type u} {a b c : α} :
a * b a * cb c
theorem le_of_add_le_add_left {α : Type u} {a b c : α} :
a + b a + cb c
@[protected, instance]
@[protected, instance]
Equations
theorem add_lt_add_left {α : Type u} {a b : α} (h : a < b) (c : α) :
c + a < c + b
theorem mul_lt_mul_left' {α : Type u} {a b : α} (h : a < b) (c : α) :
c * a < c * b
theorem mul_lt_mul_right' {α : Type u} {a b : α} (h : a < b) (c : α) :
a * c < b * c
theorem add_lt_add_right {α : Type u} {a b : α} (h : a < b) (c : α) :
a + c < b + c
theorem mul_lt_mul''' {α : Type u} {a b c d : α} (h₁ : a < b) (h₂ : c < d) :
a * c < b * d
theorem add_lt_add {α : Type u} {a b c d : α} (h₁ : a < b) (h₂ : c < d) :
a + c < b + d
theorem mul_lt_mul_of_le_of_lt {α : Type u} {a b c d : α} (h₁ : a b) (h₂ : c < d) :
a * c < b * d
theorem add_lt_add_of_le_of_lt {α : Type u} {a b c d : α} (h₁ : a b) (h₂ : c < d) :
a + c < b + d
theorem add_lt_add_of_lt_of_le {α : Type u} {a b c d : α} (h₁ : a < b) (h₂ : c d) :
a + c < b + d
theorem mul_lt_mul_of_lt_of_le {α : Type u} {a b c d : α} (h₁ : a < b) (h₂ : c d) :
a * c < b * d
theorem lt_add_of_pos_right {α : Type u} (a : α) {b : α} (h : 0 < b) :
a < a + b
theorem lt_mul_of_one_lt_right' {α : Type u} (a : α) {b : α} (h : 1 < b) :
a < a * b
theorem lt_add_of_pos_left {α : Type u} (a : α) {b : α} (h : 0 < b) :
a < b + a
theorem lt_mul_of_one_lt_left' {α : Type u} (a : α) {b : α} (h : 1 < b) :
a < b * a
theorem le_of_mul_le_mul_right' {α : Type u} {a b c : α} (h : a * b c * b) :
a c
theorem le_of_add_le_add_right {α : Type u} {a b c : α} (h : a + b c + b) :
a c
theorem mul_lt_one {α : Type u} {a b : α} (ha : a < 1) (hb : b < 1) :
a * b < 1
theorem add_neg {α : Type u} {a b : α} (ha : a < 0) (hb : b < 0) :
a + b < 0
theorem add_neg_of_neg_of_nonpos {α : Type u} {a b : α} (ha : a < 0) (hb : b 0) :
a + b < 0
theorem mul_lt_one_of_lt_one_of_le_one {α : Type u} {a b : α} (ha : a < 1) (hb : b 1) :
a * b < 1
theorem mul_lt_one_of_le_one_of_lt_one {α : Type u} {a b : α} (ha : a 1) (hb : b < 1) :
a * b < 1
theorem add_neg_of_nonpos_of_neg {α : Type u} {a b : α} (ha : a 0) (hb : b < 0) :
a + b < 0
theorem lt_add_of_pos_of_le {α : Type u} {a b c : α} (ha : 0 < a) (hbc : b c) :
b < a + c
theorem lt_mul_of_one_lt_of_le {α : Type u} {a b c : α} (ha : 1 < a) (hbc : b c) :
b < a * c
theorem lt_add_of_le_of_pos {α : Type u} {a b c : α} (hbc : b c) (ha : 0 < a) :
b < c + a
theorem lt_mul_of_le_of_one_lt {α : Type u} {a b c : α} (hbc : b c) (ha : 1 < a) :
b < c * a
theorem add_le_of_nonpos_of_le {α : Type u} {a b c : α} (ha : a 0) (hbc : b c) :
a + b c
theorem mul_le_of_le_one_of_le {α : Type u} {a b c : α} (ha : a 1) (hbc : b c) :
a * b c
theorem mul_le_of_le_of_le_one {α : Type u} {a b c : α} (hbc : b c) (ha : a 1) :
b * a c
theorem add_le_of_le_of_nonpos {α : Type u} {a b c : α} (hbc : b c) (ha : a 0) :
b + a c
theorem mul_lt_of_lt_one_of_le {α : Type u} {a b c : α} (ha : a < 1) (hbc : b c) :
a * b < c
theorem add_lt_of_neg_of_le {α : Type u} {a b c : α} (ha : a < 0) (hbc : b c) :
a + b < c
theorem add_lt_of_le_of_neg {α : Type u} {a b c : α} (hbc : b c) (ha : a < 0) :
b + a < c
theorem mul_lt_of_le_of_lt_one {α : Type u} {a b c : α} (hbc : b c) (ha : a < 1) :
b * a < c
theorem lt_mul_of_one_le_of_lt {α : Type u} {a b c : α} (ha : 1 a) (hbc : b < c) :
b < a * c
theorem lt_add_of_nonneg_of_lt {α : Type u} {a b c : α} (ha : 0 a) (hbc : b < c) :
b < a + c
theorem lt_mul_of_lt_of_one_le {α : Type u} {a b c : α} (hbc : b < c) (ha : 1 a) :
b < c * a
theorem lt_add_of_lt_of_nonneg {α : Type u} {a b c : α} (hbc : b < c) (ha : 0 a) :
b < c + a
theorem lt_mul_of_one_lt_of_lt {α : Type u} {a b c : α} (ha : 1 < a) (hbc : b < c) :
b < a * c
theorem lt_add_of_pos_of_lt {α : Type u} {a b c : α} (ha : 0 < a) (hbc : b < c) :
b < a + c
theorem lt_mul_of_lt_of_one_lt {α : Type u} {a b c : α} (hbc : b < c) (ha : 1 < a) :
b < c * a
theorem lt_add_of_lt_of_pos {α : Type u} {a b c : α} (hbc : b < c) (ha : 0 < a) :
b < c + a
theorem mul_lt_of_le_one_of_lt {α : Type u} {a b c : α} (ha : a 1) (hbc : b < c) :
a * b < c
theorem add_lt_of_nonpos_of_lt {α : Type u} {a b c : α} (ha : a 0) (hbc : b < c) :
a + b < c
theorem add_lt_of_lt_of_nonpos {α : Type u} {a b c : α} (hbc : b < c) (ha : a 0) :
b + a < c
theorem mul_lt_of_lt_of_le_one {α : Type u} {a b c : α} (hbc : b < c) (ha : a 1) :
b * a < c
theorem add_lt_of_neg_of_lt {α : Type u} {a b c : α} (ha : a < 0) (hbc : b < c) :
a + b < c
theorem mul_lt_of_lt_one_of_lt {α : Type u} {a b c : α} (ha : a < 1) (hbc : b < c) :
a * b < c
theorem mul_lt_of_lt_of_lt_one {α : Type u} {a b c : α} (hbc : b < c) (ha : a < 1) :
b * a < c
theorem add_lt_of_lt_of_neg {α : Type u} {a b c : α} (hbc : b < c) (ha : a < 0) :
b + a < c
@[simp]
theorem mul_le_mul_iff_left {α : Type u} (a : α) {b c : α} :
a * b a * c b c
@[simp]
theorem add_le_add_iff_left {α : Type u} (a : α) {b c : α} :
a + b a + c b c
@[simp]
theorem mul_le_mul_iff_right {α : Type u} {a b : α} (c : α) :
a * c b * c a b
@[simp]
theorem add_le_add_iff_right {α : Type u} {a b : α} (c : α) :
a + c b + c a b
@[simp]
theorem mul_lt_mul_iff_left {α : Type u} (a : α) {b c : α} :
a * b < a * c b < c
@[simp]
theorem add_lt_add_iff_left {α : Type u} (a : α) {b c : α} :
a + b < a + c b < c
@[simp]
theorem mul_lt_mul_iff_right {α : Type u} {a b : α} (c : α) :
a * c < b * c a < b
@[simp]
theorem add_lt_add_iff_right {α : Type u} {a b : α} (c : α) :
a + c < b + c a < b
@[simp]
theorem le_add_iff_nonneg_right {α : Type u} (a : α) {b : α} :
a a + b 0 b
@[simp]
theorem le_mul_iff_one_le_right' {α : Type u} (a : α) {b : α} :
a a * b 1 b
@[simp]
theorem le_add_iff_nonneg_left {α : Type u} (a : α) {b : α} :
a b + a 0 b
@[simp]
theorem le_mul_iff_one_le_left' {α : Type u} (a : α) {b : α} :
a b * a 1 b
@[simp]
theorem lt_add_iff_pos_right {α : Type u} (a : α) {b : α} :
a < a + b 0 < b
@[simp]
theorem lt_mul_iff_one_lt_right' {α : Type u} (a : α) {b : α} :
a < a * b 1 < b
@[simp]
theorem lt_add_iff_pos_left {α : Type u} (a : α) {b : α} :
a < b + a 0 < b
@[simp]
theorem lt_mul_iff_one_lt_left' {α : Type u} (a : α) {b : α} :
a < b * a 1 < b
@[simp]
theorem add_le_iff_nonpos_left {α : Type u} {a b : α} :
a + b b a 0
@[simp]
theorem mul_le_iff_le_one_left' {α : Type u} {a b : α} :
a * b b a 1
@[simp]
theorem add_le_iff_nonpos_right {α : Type u} {a b : α} :
a + b a b 0
@[simp]
theorem mul_le_iff_le_one_right' {α : Type u} {a b : α} :
a * b a b 1
@[simp]
theorem add_lt_iff_neg_right {α : Type u} {a b : α} :
a + b < b a < 0
@[simp]
theorem mul_lt_iff_lt_one_right' {α : Type u} {a b : α} :
a * b < b a < 1
@[simp]
theorem add_lt_iff_neg_left {α : Type u} {a b : α} :
a + b < a b < 0
@[simp]
theorem mul_lt_iff_lt_one_left' {α : Type u} {a b : α} :
a * b < a b < 1
theorem mul_eq_one_iff_eq_one_of_one_le {α : Type u} {a b : α} (ha : 1 a) (hb : 1 b) :
a * b = 1 a = 1 b = 1
theorem add_eq_zero_iff_eq_zero_of_nonneg {α : Type u} {a b : α} (ha : 0 a) (hb : 0 b) :
a + b = 0 a = 0 b = 0
def function.injective.ordered_cancel_add_comm_monoid {α : Type u} {β : Type u_1} [has_zero β] [has_add β] (f : β → α) (hf : function.injective f) (one : f 0 = 0) (mul : ∀ (x y : β), f (x + y) = f x + f y) :

Pullback an `ordered_cancel_add_comm_monoid` under an injective map.

def function.injective.ordered_cancel_comm_monoid {α : Type u} {β : Type u_1} [has_one β] [has_mul β] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

Pullback an `ordered_cancel_comm_monoid` under an injective map.

Equations
theorem monotone.mul_strict_mono' {α : Type u} {β : Type u_1} [preorder β] {f g : β → α} (hf : monotone f) (hg : strict_mono g) :
strict_mono (λ (x : β), (f x) * g x)
theorem monotone.add_strict_mono {α : Type u} {β : Type u_1} [preorder β] {f g : β → α} (hf : monotone f) (hg : strict_mono g) :
strict_mono (λ (x : β), f x + g x)
theorem strict_mono.add_monotone {α : Type u} {β : Type u_1} [preorder β] {f g : β → α} (hf : strict_mono f) (hg : monotone g) :
strict_mono (λ (x : β), f x + g x)
theorem strict_mono.mul_monotone' {α : Type u} {β : Type u_1} [preorder β] {f g : β → α} (hf : strict_mono f) (hg : monotone g) :
strict_mono (λ (x : β), (f x) * g x)
theorem strict_mono.add_const {α : Type u} {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), f x + c)
theorem strict_mono.mul_const' {α : Type u} {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), (f x) * c)
theorem strict_mono.const_add {α : Type u} {β : Type u_1} [preorder β] {f : β → α} (hf : strict_mono f) (c : α) :
strict_mono (λ (x : β), c + f x)
theorem strict_mono.const_mul' {α : Type u} {β : 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} {a b c : with_top α} :
a < (a + c < a + b c < b)
theorem with_bot.add_lt_add_iff_left {α : Type u} {a b c : with_bot α} :
< a(a + c < a + b c < b)
theorem with_top.add_lt_add_iff_right {α : Type u} {a b c : with_top α} :
a < (c + a < b + a c < b)
theorem with_bot.add_lt_add_iff_right {α : Type u} {a b c : with_bot α} :
< a(c + a < b + a c < b)

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} [linear_order α] (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} [linear_order α] (f : α → β) (n m : α) :
f (min n m) + f (max n m) = f n + f m
theorem min_add_max {α : Type u} [linear_order α] (n m : α) :
min n m + max n m = n + m
theorem min_mul_max {α : Type u} [linear_order α] (n m : α) :
(min n m) * max n m = n * m
@[class]
structure 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)
• add_left_cancel : ∀ (a b c_1 : α), a + b = a + c_1b = c_1
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : α → α
• nsmul_zero' : (∀ (x : α), . "try_refl_tac"
• nsmul_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• 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
• 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_eq :
• decidable_lt :
• lt_of_add_lt_add_left : ∀ (a b c_1 : α), a + b < a + c_1b < c_1

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

Instances
@[instance]
@[instance]
@[instance]
@[instance]
@[class]
structure linear_ordered_cancel_comm_monoid (α : Type u) :
Type u
• mul : α → α → α
• mul_assoc : ∀ (a b c_1 : α), (a * b) * c_1 = a * b * c_1
• mul_left_cancel : ∀ (a b c_1 : α), a * b = a * c_1b = c_1
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : α → α
• npow_zero' : (∀ (x : α), . "try_refl_tac"
• npow_succ' : (∀ (n : ) (x : α), . "try_refl_tac"
• 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
• le_of_mul_le_mul_left : ∀ (a b c_1 : α), a * b a * c_1b c_1
• le_total : ∀ (a b : α), a b b a
• decidable_le :
• decidable_eq :
• decidable_lt :
• lt_of_mul_lt_mul_left : ∀ (a b c_1 : α), a * b < a * c_1b < c_1

A linearly ordered cancellative commutative monoid is a commutative monoid with a linear order in which multiplication is cancellative and monotone.

Instances
theorem min_mul_mul_left {α : Type u} (a b c : α) :
min (a * b) (a * c) = a * min b c
theorem min_add_add_left {α : Type u} (a b c : α) :
min (a + b) (a + c) = a + min b c
theorem min_add_add_right {α : Type u} (a b c : α) :
min (a + c) (b + c) = min a b + c
theorem min_mul_mul_right {α : Type u} (a b c : α) :
min (a * c) (b * c) = (min a b) * c
theorem max_add_add_left {α : Type u} (a b c : α) :
max (a + b) (a + c) = a + max b c
theorem max_mul_mul_left {α : Type u} (a b c : α) :
max (a * b) (a * c) = a * max b c
theorem max_mul_mul_right {α : Type u} (a b c : α) :
max (a * c) (b * c) = (max a b) * c
theorem max_add_add_right {α : Type u} (a b c : α) :
max (a + c) (b + c) = max a b + c
theorem min_le_add_of_nonneg_right {α : Type u} {a b : α} (hb : 0 b) :
min a b a + b
theorem min_le_mul_of_one_le_right {α : Type u} {a b : α} (hb : 1 b) :
min a b a * b
theorem min_le_add_of_nonneg_left {α : Type u} {a b : α} (ha : 0 a) :
min a b a + b
theorem min_le_mul_of_one_le_left {α : Type u} {a b : α} (ha : 1 a) :
min a b a * b
theorem max_le_mul_of_one_le {α : Type u} {a b : α} (ha : 1 a) (hb : 1 b) :
max a b a * b
theorem max_le_add_of_nonneg {α : Type u} {a b : α} (ha : 0 a) (hb : 0 b) :
max a b a + b
def function.injective.linear_ordered_cancel_comm_monoid {α : Type u} {β : Type u_1} [has_one β] [has_mul β] (f : β → α) (hf : function.injective f) (one : f 1 = 1) (mul : ∀ (x y : β), f (x * y) = (f x) * f y) :

Pullback a `linear_ordered_cancel_comm_monoid` under an injective map.

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

Pullback a `linear_ordered_cancel_add_comm_monoid` under an injective map.

@[protected, instance]
def order_dual.ordered_add_comm_monoid {α : Type u}  :
@[protected, instance]
def order_dual.ordered_comm_monoid {α : Type u}  :
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
def prod.ordered_cancel_comm_monoid {M : Type u_1} {N : Type u_2}  :
Equations
@[protected, instance]
def prod.ordered_cancel_add_comm_monoid {M : Type u_1} {N : Type u_2}  :
@[protected, instance]
def multiplicative.preorder {α : Type u} [preorder α] :
Equations
@[protected, instance]
def additive.preorder {α : Type u} [preorder α] :
Equations
@[protected, instance]
def multiplicative.partial_order {α : Type u}  :
Equations
@[protected, instance]
def additive.partial_order {α : Type u}  :
Equations
@[protected, instance]
def multiplicative.linear_order {α : Type u} [linear_order α] :
Equations
@[protected, instance]
def additive.linear_order {α : Type u} [linear_order α] :
Equations
@[protected, instance]
def multiplicative.ordered_comm_monoid {α : Type u}  :
Equations
@[protected, instance]
def additive.ordered_add_comm_monoid {α : Type u}  :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def order_dual.sub_neg_monoid {α : Type u}  :
Equations
@[protected, instance]
def order_dual.div_inv_monoid {α : Type u}  :
Equations