# Documentation

Mathlib.Algebra.Order.Monoid.Defs

# Ordered monoids #

This file provides the definitions of ordered monoids.

class OrderedCommMonoid (α : Type u_2) extends , :
Type u_2
• mul : ααα
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = x *
• mul_comm : ∀ (a b : α), a * b = b * a
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b

Multiplication is monotone in an OrderedCommMonoid.

An ordered commutative monoid is a commutative monoid with a partial order such that a ≤ b → c * a ≤ c * b (multiplication is monotone)

Instances
class OrderedAddCommMonoid (α : Type u_2) extends , :
Type u_2
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = x +
• add_comm : ∀ (a b : α), a + b = b + a
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b

Addition is monotone in an OrderedAddCommMonoid.

An ordered (additive) commutative monoid is a commutative monoid with a partial order such that a ≤ b → c + a ≤ c + b (addition is monotone)

Instances
theorem OrderedAddCommMonoid.to_covariantClass_left.proof_1 (M : Type u_1) :
CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1
instance OrderedAddCommMonoid.to_covariantClass_left (M : Type u_2) :
CovariantClass M M (fun x x_1 => x + x_1) fun x x_1 => x x_1
instance OrderedCommMonoid.to_covariantClass_left (M : Type u_2) :
CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x x_1
instance OrderedAddCommMonoid.to_covariantClass_right (M : Type u_2) :
CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1
theorem OrderedAddCommMonoid.to_covariantClass_right.proof_1 (M : Type u_1) :
CovariantClass M M (Function.swap fun x x_1 => x + x_1) fun x x_1 => x x_1
instance OrderedCommMonoid.to_covariantClass_right (M : Type u_2) :
CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x x_1
@[deprecated]
theorem bit0_pos {α : Type u} {a : α} (h : 0 < a) :
0 < bit0 a
class LinearOrderedAddCommMonoid (α : Type u_2) extends , :
Type u_2
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a
• decidableLE : DecidableRel fun x x_1 => x x_1
• decidableEq :
• decidableLT : DecidableRel fun x x_1 => x < x_1
• min_def : ∀ (a b : α), min a b = if a b then a else b
• max_def : ∀ (a b : α), max a b = if a b then b else a
• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = x +
• add_comm : ∀ (a b : α), a + b = b + a
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b

Addition is monotone in an OrderedAddCommMonoid.

A linearly ordered additive commutative monoid.

Instances
class LinearOrderedCommMonoid (α : Type u_2) extends , :
Type u_2
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a
• decidableLE : DecidableRel fun x x_1 => x x_1
• decidableEq :
• decidableLT : DecidableRel fun x x_1 => x < x_1
• min_def : ∀ (a b : α), min a b = if a b then a else b
• max_def : ∀ (a b : α), max a b = if a b then b else a
• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =
• mul : ααα
• mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
• one : α
• one_mul : ∀ (a : α), 1 * a = a
• mul_one : ∀ (a : α), a * 1 = a
• npow : αα
• npow_zero : ∀ (x : α), = 1
• npow_succ : ∀ (n : ) (x : α), Monoid.npow (n + 1) x = x *
• mul_comm : ∀ (a b : α), a * b = b * a
• mul_le_mul_left : ∀ (a b : α), a b∀ (c : α), c * a c * b

Multiplication is monotone in an OrderedCommMonoid.

A linearly ordered commutative monoid.

Instances
class LinearOrderedAddCommMonoidWithTop (α : Type u_2) extends , :
Type u_2
• le : ααProp
• lt : ααProp
• le_refl : ∀ (a : α), a a
• le_trans : ∀ (a b c : α), a bb ca c
• lt_iff_le_not_le : ∀ (a b : α), a < b a b ¬b a
• le_antisymm : ∀ (a b : α), a bb aa = b
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a
• decidableLE : DecidableRel fun x x_1 => x x_1
• decidableEq :
• decidableLT : DecidableRel fun x x_1 => x < x_1
• min_def : ∀ (a b : α), min a b = if a b then a else b
• max_def : ∀ (a b : α), max a b = if a b then b else a
• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =
• add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
• zero : α
• zero_add : ∀ (a : α), 0 + a = a
• add_zero : ∀ (a : α), a + 0 = a
• nsmul : αα
• nsmul_zero : ∀ (x : α), = 0
• nsmul_succ : ∀ (n : ) (x : α), AddMonoid.nsmul (n + 1) x = x +
• add_comm : ∀ (a b : α), a + b = b + a
• add_le_add_left : ∀ (a b : α), a b∀ (c : α), c + a c + b
• top : α
• le_top : ∀ (x : α), x

In a LinearOrderedAddCommMonoidWithTop, the ⊤ element is larger than any other element.

• top_add' : ∀ (x : α), + x =

In a LinearOrderedAddCommMonoidWithTop, the ⊤ element is invariant under addition.

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 : α) :