# mathlib3documentation

algebra.order.monoid.defs

# Ordered monoids #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides the definitions of ordered monoids.

@[instance]
@[instance]
@[class]
structure ordered_comm_monoid (α : Type u_2) :
Type u_2

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

Instances of this typeclass
Instances of other typeclasses for ordered_comm_monoid
• ordered_comm_monoid.has_sizeof_inst
@[class]
structure ordered_add_comm_monoid (α : Type u_2) :
Type u_2
• add : α α α
• 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 : α), . "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 : α), a b b c a c
• lt_iff_le_not_le : ( (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : (a b : α), a b b a a = b
• add_le_add_left : (a b : α), a b (c : α), c + a c + b

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 of this typeclass
Instances of other typeclasses for ordered_add_comm_monoid
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem bit0_pos {α : Type u} {a : α} (h : 0 < a) :
0 < bit0 a
@[instance]
@[class]
structure linear_ordered_add_comm_monoid (α : Type u_2) :
Type u_2
• le : α α Prop
• lt : α α Prop
• le_refl : (a : α), a a
• le_trans : (a b c : α), a b b c a c
• lt_iff_le_not_le : ( (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : (a b : α), a b b a a = b
• le_total : (a b : α), a b b a
• decidable_le :
• decidable_eq :
• decidable_lt :
• max : α α α
• max_def : . "reflexivity"
• min : α α α
• min_def : . "reflexivity"
• add : α α α
• 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 : α), . "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 : α), c + a c + b

A linearly ordered additive commutative monoid.

Instances of this typeclass
Instances of other typeclasses for linear_ordered_add_comm_monoid
@[class]
structure linear_ordered_comm_monoid (α : Type u_2) :
Type u_2
• le : α α Prop
• lt : α α Prop
• le_refl : (a : α), a a
• le_trans : (a b c : α), a b b c a c
• lt_iff_le_not_le : ( (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : (a b : α), a b b a a = b
• le_total : (a b : α), a b b a
• decidable_le :
• decidable_eq :
• decidable_lt :
• max : α α α
• max_def : . "reflexivity"
• min : α α α
• min_def : . "reflexivity"
• 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 : α), . "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 : α), c * a c * b

A linearly ordered commutative monoid.

Instances of this typeclass
Instances of other typeclasses for linear_ordered_comm_monoid
• linear_ordered_comm_monoid.has_sizeof_inst
@[instance]
@[class]
structure linear_ordered_add_comm_monoid_with_top (α : Type u_2) :
Type u_2
• le : α α Prop
• lt : α α Prop
• le_refl : (a : α), a a
• le_trans : (a b c : α), a b b c a c
• lt_iff_le_not_le : ( (a b : α), a < b a b ¬b a) . "order_laws_tac"
• le_antisymm : (a b : α), a b b a a = b
• le_total : (a b : α), a b b a
• decidable_le :
• decidable_eq :
• decidable_lt :
• max : α α α
• max_def : . "reflexivity"
• min : α α α
• min_def : . "reflexivity"
• add : α α α
• 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 : α), . "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 : α), c + a c + b
• top : α
• le_top : (x : α), x
• 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 of this typeclass
Instances of other typeclasses for linear_ordered_add_comm_monoid_with_top`