# mathlib3documentation

algebra.order.monoid.cancel.defs

# Ordered cancellative monoids #

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

@[class]
structure ordered_cancel_add_comm_monoid (α : Type u) :
• 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
• le_of_add_le_add_left : (a b c : α), a + b a + c b c

An ordered cancellative additive commutative monoid is an additive commutative monoid with a partial order, in which addition is cancellative and monotone.

Instances of this typeclass
Instances of other typeclasses for ordered_cancel_add_comm_monoid
@[class]
structure ordered_cancel_comm_monoid (α : Type u) :

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

Instances of this typeclass
Instances of other typeclasses for ordered_cancel_comm_monoid
• ordered_cancel_comm_monoid.has_sizeof_inst
@[protected, instance]
@[protected, instance]
a + b < a + c b < c
theorem ordered_cancel_comm_monoid.lt_of_mul_lt_mul_left {α : Type u} (a b c : α) :
a * b < a * c b < c
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[class]
• 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
• le_of_add_le_add_left : (a b c : α), a + b a + c b c
• le_total : (a b : α), a b b a
• decidable_le :
• decidable_eq :
• decidable_lt :
• max : α α α
• max_def : . "reflexivity"
• min : α α α
• min_def : . "reflexivity"

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 of this typeclass
Instances of other typeclasses for linear_ordered_cancel_add_comm_monoid
@[instance]
@[instance]
@[instance]
@[instance]
@[class]
structure linear_ordered_cancel_comm_monoid (α : Type u) :
• 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
• 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
• mul_le_mul_left : (a b : α), a b (c : α), c * a c * b
• le_of_mul_le_mul_left : (a b c : α), a * b a * c b c
• le_total : (a b : α), a b b a
• decidable_le :
• decidable_eq :
• decidable_lt :
• max : α α α
• max_def : . "reflexivity"
• min : α α α
• min_def : . "reflexivity"

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

Instances of this typeclass
Instances of other typeclasses for linear_ordered_cancel_comm_monoid
• linear_ordered_cancel_comm_monoid.has_sizeof_inst