# mathlib3documentation

algebra.order.monoid.canonical.defs

# Canonically ordered monoids #

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

@[class]
structure has_exists_mul_of_le (α : Type u) [has_mul α] [has_le α] :
Prop

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 of this typeclass
@[class]
Prop

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 of this typeclass
@[protected, instance]
def group.has_exists_mul_of_le (α : Type u) [group α] [has_le α] :
@[protected, instance]
theorem exists_one_lt_mul_of_lt' {α : Type u} [preorder α] {a b : α} (h : a < b) :
(c : α), 1 < c a * c = b
theorem exists_pos_add_of_lt' {α : Type u} [preorder α] {a b : α} (h : a < b) :
(c : α), 0 < c a + c = b
theorem le_of_forall_one_lt_le_mul {α : Type u} [linear_order α] [monoid α] {a b : α} (h : (ε : α), 1 < ε a b * ε) :
a b
theorem le_of_forall_pos_le_add {α : Type u} [linear_order α] [add_monoid α] {a b : α} (h : (ε : α), 0 < ε a b + ε) :
a b
theorem le_of_forall_pos_lt_add' {α : Type u} [linear_order α] [add_monoid α] {a b : α} (h : (ε : α), 0 < ε a < b + ε) :
a b
theorem le_of_forall_one_lt_lt_mul' {α : Type u} [linear_order α] [monoid α] {a b : α} (h : (ε : α), 1 < ε a < b * ε) :
a b
theorem le_iff_forall_pos_lt_add' {α : Type u} [linear_order α] [add_monoid α] {a b : α} :
a b (ε : α), 0 < ε a < b + ε
theorem le_iff_forall_one_lt_lt_mul' {α : Type u} [linear_order α] [monoid α] {a b : α} :
a b (ε : α), 1 < ε a < b * ε
@[instance]
@[class]
structure canonically_ordered_add_monoid (α : Type u_1) :
Type u_1
• 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
• bot : α
• bot_le : (x : α), x
• exists_add_of_le : {a b : α}, a b ( (c : α), b = a + c)
• le_self_add : (a b : α), a a + b

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_groups.

Instances of this typeclass
Instances of other typeclasses for canonically_ordered_add_monoid
@[protected, instance]
Equations
@[class]
structure canonically_ordered_monoid (α : Type u_1) :
Type u_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. Examples 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 of this typeclass
Instances of other typeclasses for canonically_ordered_monoid
• canonically_ordered_monoid.has_sizeof_inst
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
theorem le_self_mul {α : Type u} {a c : α} :
a a * c
theorem le_self_add {α : Type u} {a c : α} :
a a + c
theorem le_mul_self {α : Type u} {a b : α} :
a b * a
theorem le_add_self {α : Type u} {a b : α} :
a b + a
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
theorem le_of_mul_le_left {α : Type u} {a b c : α} :
a * b c a c
theorem le_of_add_le_left {α : Type u} {a b c : α} :
a + b c a c
theorem le_of_add_le_right {α : Type u} {a b c : α} :
a + b c b c
theorem le_of_mul_le_right {α : Type u} {a b c : α} :
a * b c b c
theorem le_mul_of_le_left {α : Type u} {a b c : α} :
a b a b * c
theorem le_add_of_le_left {α : Type u} {a b c : α} :
a b a b + c
theorem le_add_of_le_right {α : Type u} {a b c : α} :
a c a b + c
theorem le_mul_of_le_right {α : Type u} {a b c : α} :
a c a b * c
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 le_iff_exists_add' {α : Type u} {a b : α} :
a b (c : α), b = c + a
theorem le_iff_exists_mul' {α : Type u} {a b : α} :
a b (c : α), b = c * a
@[simp]
theorem one_le {α : Type u} (a : α) :
1 a
@[simp]
theorem zero_le {α : Type u} (a : α) :
0 a
theorem bot_eq_one {α : Type u}  :
= 1
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 eq_zero_or_pos {α : Type u} {a : α} :
a = 0 0 < a
theorem eq_one_or_one_lt {α : Type u} {a : α} :
a = 1 1 < a
@[simp]
theorem one_lt_mul_iff {α : Type u} {a b : α} :
1 < a * b 1 < a 1 < b
@[simp]
theorem add_pos_iff {α : Type u} {a b : α} :
0 < a + b 0 < a 0 < b
theorem exists_one_lt_mul_of_lt {α : Type u} {a b : α} (h : a < b) :
(c : α) (hc : 1 < c), a * c = b
theorem exists_pos_add_of_lt {α : Type u} {a b : α} (h : a < b) :
(c : α) (hc : 0 < c), 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
theorem lt_iff_exists_mul {α : Type u} {a b : α}  :
a < b (c : α) (H : c > 1), b = a * c
theorem lt_iff_exists_add {α : Type u} {a b : α}  :
a < b (c : α) (H : c > 0), b = a + c
theorem pos_of_gt {M : Type u_1} {n m : M} (h : n < m) :
0 < m
theorem ne_zero.pos {M : Type u_1} (a : M) [ne_zero a] :
0 < a
theorem ne_zero.of_gt {M : Type u_1} {x y : M} (h : x < y) :
@[protected, instance]
def ne_zero.of_gt' {M : Type u_1} [has_one M] {y : M} [fact (1 < y)] :
@[protected, instance]
def ne_zero.bit0 {M : Type u_1} {x : M} [ne_zero x] :
@[instance]
@[class]
structure canonically_linear_ordered_add_monoid (α : Type u_1) :
Type u_1
• 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
• bot : α
• bot_le : (x : α), x
• exists_add_of_le : {a b : α}, a b ( (c : α), b = a + c)
• le_self_add : (a 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"

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

Instances of this typeclass
Instances of other typeclasses for canonically_linear_ordered_add_monoid
@[instance]
@[class]
structure canonically_linear_ordered_monoid (α : Type u_1) :
Type u_1
• 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
• bot : α
• bot_le : (x : α), x
• exists_mul_of_le : {a b : α}, a b ( (c : α), b = a * c)
• le_self_mul : (a 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"

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

Instances of this typeclass
Instances of other typeclasses for canonically_linear_ordered_monoid
• canonically_linear_ordered_monoid.has_sizeof_inst
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem min_add_distrib {α : Type u} (a b c : α) :
(b + c) = b + c)
theorem min_mul_distrib {α : Type u} (a b c : α) :
(b * c) = b * c)
theorem min_mul_distrib' {α : Type u} (a b c : α) :
linear_order.min (a * b) c = c
theorem min_add_distrib' {α : Type u} (a b c : α) :
linear_order.min (a + b) c = c
@[simp]
theorem one_min {α : Type u} (a : α) :
= 1
@[simp]
theorem zero_min {α : Type u} (a : α) :
= 0
@[simp]
theorem min_zero {α : Type u} (a : α) :
= 0
@[simp]
theorem min_one {α : Type u} (a : α) :
= 1
@[simp]
theorem bot_eq_one' {α : Type u}  :
= 1

In a linearly ordered monoid, we are happy for bot_eq_one to be a @[simp] lemma.

@[simp]
theorem bot_eq_zero' {α : Type u}  :
= 0

In a linearly ordered monoid, we are happy for bot_eq_zero to be a @[simp] lemma