# Documentation

Mathlib.Algebra.Order.Monoid.Canonical.Defs

# Canonically ordered monoids #

class ExistsMulOfLE (α : Type u) [Mul α] [LE α] :
• exists_mul_of_le : ∀ {a b : α}, a bc, b = a * c

For a ≤ b, a left divides b

An OrderedCommMonoid 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 CanonicallyOrderedMonoid.

Instances
• exists_add_of_le : ∀ {a b : α}, a bc, b = a + c

For a ≤ b, there is a c so b = a + c.

An OrderedAddCommMonoid 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 CanonicallyOrderedAddMonoid.

Instances
instance Group.existsMulOfLE (α : Type u) [] [LE α] :
theorem exists_pos_add_of_lt' {α : Type u} [] [] [ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [] {a : α} {b : α} (h : a < b) :
c, 0 < c a + c = b
theorem exists_one_lt_mul_of_lt' {α : Type u} [] [] [ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [] {a : α} {b : α} (h : a < b) :
c, 1 < c a * c = b
theorem le_of_forall_pos_le_add {α : Type u} [] [] [] [] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : ∀ (ε : α), 0 < εa b + ε) :
a b
theorem le_of_forall_one_lt_le_mul {α : Type u} [] [] [] [] [CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : ∀ (ε : α), 1 < εa b * ε) :
a b
theorem le_of_forall_pos_lt_add' {α : Type u} [] [] [] [] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : ∀ (ε : α), 0 < εa < b + ε) :
a b
theorem le_of_forall_one_lt_lt_mul' {α : Type u} [] [] [] [] [CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} (h : ∀ (ε : α), 1 < εa < b * ε) :
a b
theorem le_iff_forall_pos_lt_add' {α : Type u} [] [] [] [] [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] [ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
a b ∀ (ε : α), 0 < εa < b + ε
theorem le_iff_forall_one_lt_lt_mul' {α : Type u} [] [] [] [] [CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] [ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] {a : α} {b : α} :
a b ∀ (ε : α), 1 < εa < b * ε
class CanonicallyOrderedAddMonoid (α : Type u_1) extends , :
Type u_1
• 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
• bot : α
• bot_le : ∀ (x : α), x

⊥ is the least element

• exists_add_of_le : ∀ {a b : α}, a bc, b = a + c

For a ≤ b, there is a c so b = a + c.

• le_self_add : ∀ (a b : α), a a + b

For any a and 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 OrderedAddCommGroups.

Instances
class CanonicallyOrderedMonoid (α : Type u_1) extends , :
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 : α), = 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
• bot : α
• bot_le : ∀ (x : α), x

⊥ is the least element

• exists_mul_of_le : ∀ {a b : α}, a bc, b = a * c

For a ≤ b, there is a c so b = a * c.

• le_self_mul : ∀ (a b : α), a a * b

For any a and b, a ≤ a * b

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 OrderDual 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_self_add {α : Type u} {a : α} {c : α} :
a a + c
theorem le_self_mul {α : Type u} {a : α} {c : α} :
a a * c
theorem le_add_self {α : Type u} {a : α} {b : α} :
a b + a
theorem le_mul_self {α : Type u} {a : α} {b : α} :
a b * a
@[simp]
theorem self_le_add_right {α : Type u} (a : α) (b : α) :
a a + b
@[simp]
theorem self_le_mul_right {α : Type u} (a : α) (b : α) :
a a * b
@[simp]
theorem self_le_add_left {α : Type u} (a : α) (b : α) :
a b + a
@[simp]
theorem self_le_mul_left {α : Type u} (a : α) (b : α) :
a b * a
theorem le_of_add_le_left {α : Type u} {a : α} {b : α} {c : α} :
a + b ca c
theorem le_of_mul_le_left {α : Type u} {a : α} {b : α} {c : α} :
a * b ca c
theorem le_of_add_le_right {α : Type u} {a : α} {b : α} {c : α} :
a + b cb c
theorem le_of_mul_le_right {α : Type u} {a : α} {b : α} {c : α} :
a * b cb c
theorem le_add_of_le_left {α : Type u} {a : α} {b : α} {c : α} :
a ba b + c
theorem le_mul_of_le_left {α : Type u} {a : α} {b : α} {c : α} :
a ba b * c
theorem le_add_of_le_right {α : Type u} {a : α} {b : α} {c : α} :
a ca b + c
theorem le_mul_of_le_right {α : Type u} {a : α} {b : α} {c : α} :
a ca 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 zero_le {α : Type u} (a : α) :
0 a
@[simp]
theorem one_le {α : Type u} (a : α) :
1 a
theorem bot_eq_zero {α : Type u} :
= 0
theorem bot_eq_one {α : Type u} :
= 1
@[simp]
theorem add_eq_zero_iff {α : Type u} {a : α} {b : α} :
a + b = 0 a = 0 b = 0
@[simp]
theorem mul_eq_one_iff {α : Type u} {a : α} {b : α} :
a * b = 1 a = 1 b = 1
@[simp]
theorem nonpos_iff_eq_zero {α : Type u} {a : α} :
a 0 a = 0
@[simp]
theorem le_one_iff_eq_one {α : Type u} {a : α} :
a 1 a = 1
theorem pos_iff_ne_zero {α : Type u} {a : α} :
0 < a a 0
theorem one_lt_iff_ne_one {α : Type u} {a : α} :
1 < a a 1
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 add_pos_iff {α : Type u} {a : α} {b : α} :
0 < a + b 0 < a 0 < b
@[simp]
theorem one_lt_mul_iff {α : Type u} {a : α} {b : α} :
1 < a * b 1 < a 1 < b
theorem exists_pos_add_of_lt {α : Type u} {a : α} {b : α} (h : a < b) :
c x, a + c = b
theorem exists_one_lt_mul_of_lt {α : Type u} {a : α} {b : α} (h : a < b) :
c x, 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_add {α : Type u} {a : α} {b : α} [CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] :
a < b c, c > 0 b = a + c
theorem lt_iff_exists_mul {α : Type u} {a : α} {b : α} [CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1] :
a < b c, c > 1 b = a * c
theorem pos_of_gt {M : Type u_1} {n : M} {m : M} (h : n < m) :
0 < m
theorem NeZero.pos {M : Type u_1} (a : M) [] :
0 < a
theorem NeZero.of_gt {M : Type u_1} {x : M} {y : M} (h : x < y) :
instance NeZero.of_gt' {M : Type u_1} [One M] {y : M} [Fact (1 < y)] :
instance NeZero.bit0 {M : Type u_1} {x : M} [] :
class CanonicallyLinearOrderedAddMonoid (α : Type u_1) extends , , , :
Type u_1
• 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
• bot : α
• bot_le : ∀ (x : α), x
• exists_add_of_le : ∀ {a b : α}, a bc, b = a + c
• le_self_add : ∀ (a b : α), a a + b
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a

A linear order is total.

• decidableLE : DecidableRel fun x x_1 => x x_1

In a linearly ordered type, we assume the order relations are all decidable.

• decidableEq :

In a linearly ordered type, we assume the order relations are all decidable.

• decidableLT : DecidableRel fun x x_1 => x < x_1

In a linearly ordered type, we assume the order relations are all decidable.

• min_def : ∀ (a b : α), min a b = if a b then a else b

The minimum function is equivalent to the one you get from minOfLe.

• max_def : ∀ (a b : α), max a b = if a b then b else a

The minimum function is equivalent to the one you get from maxOfLe.

• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =

Comparison via compare is equal to the canonical comparison given decidable < and =.

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

Instances
class CanonicallyLinearOrderedMonoid (α : Type u_1) extends , , , :
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 : α), = 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
• bot : α
• bot_le : ∀ (x : α), x
• exists_mul_of_le : ∀ {a b : α}, a bc, b = a * c
• le_self_mul : ∀ (a b : α), a a * b
• min : ααα
• max : ααα
• compare : ααOrdering
• le_total : ∀ (a b : α), a b b a

A linear order is total.

• decidableLE : DecidableRel fun x x_1 => x x_1

In a linearly ordered type, we assume the order relations are all decidable.

• decidableEq :

In a linearly ordered type, we assume the order relations are all decidable.

• decidableLT : DecidableRel fun x x_1 => x < x_1

In a linearly ordered type, we assume the order relations are all decidable.

• min_def : ∀ (a b : α), min a b = if a b then a else b

The minimum function is equivalent to the one you get from minOfLe.

• max_def : ∀ (a b : α), max a b = if a b then b else a

The minimum function is equivalent to the one you get from maxOfLe.

• compare_eq_compareOfLessAndEq : ∀ (a b : α), compare a b =

Comparison via compare is equal to the canonical comparison given decidable < and =.

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

Instances
theorem CanonicallyLinearOrderedAddMonoid.semilatticeSup.proof_3 {α : Type u_1} (a : α) (b : α) (c : α) :
a cb ca b c
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_add_distrib' {α : Type u} (a : α) (b : α) (c : α) :
min (a + b) c = min (min a c + min b c) c
theorem min_mul_distrib' {α : Type u} (a : α) (b : α) (c : α) :
min (a * b) c = min (min a c * min b c) c
theorem zero_min {α : Type u} (a : α) :
min 0 a = 0
theorem one_min {α : Type u} (a : α) :
min 1 a = 1
theorem min_zero {α : Type u} (a : α) :
min a 0 = 0
theorem min_one {α : Type u} (a : α) :
min a 1 = 1
@[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

@[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.