# 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
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[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 : α) :
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. See note [reducible non-instances].

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.

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. See note [reducible non-instances].

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
@[instance]
@[instance]
def units.preorder {α : Type u} [monoid α] [preorder α] :
Equations
@[simp]
a b a b
@[simp]
theorem units.coe_le_coe {α : Type u} [monoid α] [preorder α] {a b : units α} :
a b a b
@[simp]
a < b a < b
@[simp]
theorem units.coe_lt_coe {α : Type u} [monoid α] [preorder α] {a b : units α} :
a < b a < b
@[instance]
@[instance]
def units.partial_order {α : Type u} [monoid α]  :
Equations
@[instance]
def units.linear_order {α : Type u} [monoid α] [linear_order α] :
Equations
@[instance]
@[simp]
(max a b) = max a b
@[simp]
theorem units.max_coe {α : Type u} [monoid α] [linear_order α] {a b : units α} :
(max a b) = max a b
@[simp]
theorem units.min_coe {α : Type u} [monoid α] [linear_order α] {a b : units α} :
(min a b) = min a b
@[simp]
(min a b) = min a b
@[instance]
def with_zero.preorder {α : Type u} [preorder α] :
Equations
@[instance]
def with_zero.partial_order {α : Type u}  :
Equations
@[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} [preorder α] (a : α) :
0 < a
@[simp]
theorem with_zero.coe_lt_coe {α : Type u} {a b : α} :
a < b a < b
@[simp]
theorem with_zero.coe_le_coe {α : Type u} {a b : α} :
a b a b
@[instance]
def with_zero.lattice {α : Type u} [lattice α] :
Equations
@[instance]
def with_zero.linear_order {α : Type u} [linear_order α] :
Equations
theorem with_zero.mul_le_mul_left {α : Type u} [has_mul α] [preorder α] (a b : with_zero α) :
a b∀ (c : , c * a c * b
theorem with_zero.lt_of_mul_lt_mul_left {α : Type u} [has_mul α] (a b c : with_zero α) :
a * b < a * cb < c
@[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
@[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]
Equations
@[instance]
def with_top.add_semigroup {α : Type u}  :
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 : α} :
(bit0 a) =
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
@[instance]
def with_top.add_comm_semigroup {α : Type u}  :
Equations
@[instance]
Equations
@[instance]
def with_top.add_comm_monoid {α : Type u}  :
Equations
@[instance]
def with_top.ordered_add_comm_monoid {α : Type u}  :
Equations
@[instance]
Equations
α →+

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

Equations
@[simp]
@[simp]
theorem with_top.zero_lt_top {α : Type u}  :
0 <
@[simp]
theorem with_top.zero_lt_coe {α : Type u} (a : α) :
0 < a 0 < a
@[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_semigroup {α : Type u}  :
Equations
@[instance]
def with_bot.add_comm_semigroup {α : Type u}  :
Equations
@[instance]
Equations
@[instance]
def with_bot.add_comm_monoid {α : Type u}  :
Equations
@[instance]
def with_bot.ordered_add_comm_monoid {α : Type u}  :
Equations
@[instance]
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_mul_self {α : Type u} {a b : α} :
a b * a
theorem le_add_self {α : Type u} {a b : α} :
a b + a
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
theorem le_self_mul {α : Type u} {a c : α} :
a a * c
theorem le_self_add {α : Type u} {a c : α} :
a a + c
@[instance]

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

Equations
@[instance]
@[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.

@[instance]
@[instance]
Equations
@[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
@[instance]
@[instance]
Equations
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. See note [reducible non-instances].

Equations
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. See note [reducible non-instances].

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.

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