mathlib documentation

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]
structure has_exists_add_of_le (α : Type u) [has_add α] [has_le α] :
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]
@[protected, instance]
theorem exists_one_lt_mul_of_lt' {α : Type u} [mul_one_class α] [preorder α] [contravariant_class α α has_mul.mul has_lt.lt] [has_exists_mul_of_le α] {a b : α} (h : a < b) :
(c : α), 1 < c a * c = b
theorem exists_pos_add_of_lt' {α : Type u} [add_zero_class α] [preorder α] [contravariant_class α α has_add.add has_lt.lt] [has_exists_add_of_le α] {a b : α} (h : a < b) :
(c : α), 0 < c a + c = b
theorem le_of_forall_one_lt_le_mul {α : Type u} [linear_order α] [densely_ordered α] [monoid α] [has_exists_mul_of_le α] [covariant_class α α has_mul.mul has_lt.lt] [contravariant_class α α has_mul.mul has_lt.lt] {a b : α} (h : (ε : α), 1 < ε a b * ε) :
a b
theorem le_of_forall_pos_le_add {α : Type u} [linear_order α] [densely_ordered α] [add_monoid α] [has_exists_add_of_le α] [covariant_class α α has_add.add has_lt.lt] [contravariant_class α α has_add.add has_lt.lt] {a b : α} (h : (ε : α), 0 < ε a b + ε) :
a b
theorem le_of_forall_pos_lt_add' {α : Type u} [linear_order α] [densely_ordered α] [add_monoid α] [has_exists_add_of_le α] [covariant_class α α has_add.add has_lt.lt] [contravariant_class α α has_add.add has_lt.lt] {a b : α} (h : (ε : α), 0 < ε a < b + ε) :
a b
theorem le_of_forall_one_lt_lt_mul' {α : Type u} [linear_order α] [densely_ordered α] [monoid α] [has_exists_mul_of_le α] [covariant_class α α has_mul.mul has_lt.lt] [contravariant_class α α has_mul.mul has_lt.lt] {a b : α} (h : (ε : α), 1 < ε a < b * ε) :
a b
@[class]
structure canonically_ordered_add_monoid (α : Type u_1) :
Type u_1

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
  • canonically_ordered_add_monoid.has_sizeof_inst
@[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
theorem le_self_mul {α : Type u} [canonically_ordered_monoid α] {a c : α} :
a a * c
theorem le_self_add {α : Type u} [canonically_ordered_add_monoid α] {a c : α} :
a a + c
theorem le_mul_self {α : Type u} [canonically_ordered_monoid α] {a b : α} :
a b * a
theorem le_add_self {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :
a b + a
theorem self_le_mul_right {α : Type u} [canonically_ordered_monoid α] (a b : α) :
a a * b
theorem self_le_add_right {α : Type u} [canonically_ordered_add_monoid α] (a b : α) :
a a + b
theorem self_le_add_left {α : Type u} [canonically_ordered_add_monoid α] (a b : α) :
a b + a
theorem self_le_mul_left {α : Type u} [canonically_ordered_monoid α] (a b : α) :
a b * a
theorem le_of_mul_le_left {α : Type u} [canonically_ordered_monoid α] {a b c : α} :
a * b c a c
theorem le_of_add_le_left {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} :
a + b c a c
theorem le_of_add_le_right {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} :
a + b c b c
theorem le_of_mul_le_right {α : Type u} [canonically_ordered_monoid α] {a b c : α} :
a * b c b c
theorem le_iff_exists_add {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :
a b (c : α), b = a + c
theorem le_iff_exists_mul {α : Type u} [canonically_ordered_monoid α] {a b : α} :
a b (c : α), b = a * c
theorem le_iff_exists_add' {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :
a b (c : α), b = c + a
theorem le_iff_exists_mul' {α : Type u} [canonically_ordered_monoid α] {a b : α} :
a b (c : α), b = c * a
@[simp]
theorem one_le {α : Type u} [canonically_ordered_monoid α] (a : α) :
1 a
@[simp]
theorem zero_le {α : Type u} [canonically_ordered_add_monoid α] (a : α) :
0 a
theorem bot_eq_one {α : Type u} [canonically_ordered_monoid α] :
= 1
@[simp]
theorem mul_eq_one_iff {α : Type u} [canonically_ordered_monoid α] {a b : α} :
a * b = 1 a = 1 b = 1
@[simp]
theorem add_eq_zero_iff {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :
a + b = 0 a = 0 b = 0
@[simp]
theorem le_one_iff_eq_one {α : Type u} [canonically_ordered_monoid α] {a : α} :
a 1 a = 1
@[simp]
theorem nonpos_iff_eq_zero {α : Type u} [canonically_ordered_add_monoid α] {a : α} :
a 0 a = 0
theorem one_lt_iff_ne_one {α : Type u} [canonically_ordered_monoid α] {a : α} :
1 < a a 1
theorem pos_iff_ne_zero {α : Type u} [canonically_ordered_add_monoid α] {a : α} :
0 < a a 0
theorem eq_zero_or_pos {α : Type u} [canonically_ordered_add_monoid α] {a : α} :
a = 0 0 < a
theorem eq_one_or_one_lt {α : Type u} [canonically_ordered_monoid α] {a : α} :
a = 1 1 < a
@[simp]
theorem one_lt_mul_iff {α : Type u} [canonically_ordered_monoid α] {a b : α} :
1 < a * b 1 < a 1 < b
@[simp]
theorem add_pos_iff {α : Type u} [canonically_ordered_add_monoid α] {a b : α} :
0 < a + b 0 < a 0 < b
theorem exists_one_lt_mul_of_lt {α : Type u} [canonically_ordered_monoid α] {a b : α} (h : a < b) :
(c : α) (hc : 1 < c), a * c = b
theorem exists_pos_add_of_lt {α : Type u} [canonically_ordered_add_monoid α] {a b : α} (h : a < b) :
(c : α) (hc : 0 < c), a + c = b
theorem le_add_left {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} (h : a c) :
a b + c
theorem le_mul_left {α : Type u} [canonically_ordered_monoid α] {a b c : α} (h : a c) :
a b * c
theorem le_add_right {α : Type u} [canonically_ordered_add_monoid α] {a b c : α} (h : a b) :
a b + c
theorem le_mul_right {α : Type u} [canonically_ordered_monoid α] {a b c : α} (h : a b) :
a b * c
theorem lt_iff_exists_mul {α : Type u} [canonically_ordered_monoid α] {a b : α} [covariant_class α α has_mul.mul has_lt.lt] :
a < b (c : α) (H : c > 1), b = a * c
theorem lt_iff_exists_add {α : Type u} [canonically_ordered_add_monoid α] {a b : α} [covariant_class α α has_add.add has_lt.lt] :
a < b (c : α) (H : c > 0), b = a + c
theorem pos_of_gt {M : Type u_1} [canonically_ordered_add_monoid M] {n m : M} (h : n < m) :
0 < m
theorem ne_zero.pos {M : Type u_1} (a : M) [canonically_ordered_add_monoid M] [ne_zero a] :
0 < a
theorem ne_zero.of_gt {M : Type u_1} [canonically_ordered_add_monoid M] {x y : M} (h : x < y) :
@[protected, instance]
def ne_zero.of_gt' {M : Type u_1} [canonically_ordered_add_monoid M] [has_one M] {y : M} [fact (1 < y)] :
@[protected, instance]
def ne_zero.bit0 {M : Type u_1} [canonically_ordered_add_monoid M] {x : M} [ne_zero x] :
@[class]
structure canonically_linear_ordered_add_monoid (α : Type u_1) :
Type u_1

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
  • canonically_linear_ordered_add_monoid.has_sizeof_inst
@[class]
structure canonically_linear_ordered_monoid (α : Type u_1) :
Type u_1

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
@[simp]
theorem one_min {α : Type u} [canonically_linear_ordered_monoid α] (a : α) :
@[simp]
theorem zero_min {α : Type u} [canonically_linear_ordered_add_monoid α] (a : α) :
@[simp]
theorem min_zero {α : Type u} [canonically_linear_ordered_add_monoid α] (a : α) :
@[simp]
theorem min_one {α : Type u} [canonically_linear_ordered_monoid α] (a : α) :
@[simp]

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

@[simp]

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