Canonically ordered monoids

class CanonicallyOrderedAdd (α : Type u_1) [Add α] [LE α] extends ExistsAddOfLE α : Prop

An ordered additive monoid is CanonicallyOrderedAdd if 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.

• exists_add_of_le {a b : α} : a ≤ b → ∃ (c : α), b = a + c
• le_self_add (a b : α) : a ≤ a + b

  For any a and b, a ≤ a + b

class CanonicallyOrderedMul (α : Type u_1) [Mul α] [LE α] extends ExistsMulOfLE α : Prop

An ordered monoid is CanonicallyOrderedMul if 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).

• exists_mul_of_le {a b : α} : a ≤ b → ∃ (c : α), b = a * c
• le_self_mul (a b : α) : a ≤ a * b

  For any a and b, a ≤ a * b

@[deprecated "Use `[OrderedAddCommMonoid α] [CanonicallyOrderedAdd α]` instead." (since := "2025-01-13")]

structure CanonicallyOrderedAddCommMonoid (α : Type u_1) extends OrderedAddCommMonoid α, OrderBot α : 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 OrderedAddCommGroups.

• 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 : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• 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 (a : α) : ⊥ ≤ a
• exists_add_of_le {a b : α} : a ≤ b → ∃ (c : α), 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

@[deprecated "Use `[OrderedCommMonoid α] [CanonicallyOrderedMul α]` instead." (since := "2025-01-13")]

structure CanonicallyOrderedCommMonoid (α : Type u_1) extends OrderedCommMonoid α, OrderBot α : 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 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).

• 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 : α) : Monoid.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Monoid.npow (n + 1) x = Monoid.npow n 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• 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 (a : α) : ⊥ ≤ a
• exists_mul_of_le {a b : α} : a ≤ b → ∃ (c : α), 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

theorem le_self_mul {α : Type u} [Mul α] [LE α] [CanonicallyOrderedMul α] {a b : α} : a ≤ a * b

theorem le_self_add {α : Type u} [Add α] [LE α] [CanonicallyOrderedAdd α] {a b : α} : a ≤ a + b

@[simp]

theorem self_le_mul_right {α : Type u} [Mul α] [LE α] [CanonicallyOrderedMul α] (a b : α) : a ≤ a * b

@[simp]

theorem self_le_add_right {α : Type u} [Add α] [LE α] [CanonicallyOrderedAdd α] (a b : α) : a ≤ a + b

theorem le_iff_exists_mul {α : Type u} [Mul α] [LE α] [CanonicallyOrderedMul α] {a b : α} : a ≤ b ↔ ∃ (c : α), b = a * c

theorem le_iff_exists_add {α : Type u} [Add α] [LE α] [CanonicallyOrderedAdd α] {a b : α} : a ≤ b ↔ ∃ (c : α), b = a + c

theorem le_of_mul_le_left {α : Type u} [Mul α] [Preorder α] [CanonicallyOrderedMul α] {a b c : α} : a * b ≤ c → a ≤ c

theorem le_of_add_le_left {α : Type u} [Add α] [Preorder α] [CanonicallyOrderedAdd α] {a b c : α} : a + b ≤ c → a ≤ c

theorem le_mul_of_le_left {α : Type u} [Mul α] [Preorder α] [CanonicallyOrderedMul α] {a b c : α} : a ≤ b → a ≤ b * c

theorem le_add_of_le_left {α : Type u} [Add α] [Preorder α] [CanonicallyOrderedAdd α] {a b c : α} : a ≤ b → a ≤ b + c

theorem le_mul_right {α : Type u} [Mul α] [Preorder α] [CanonicallyOrderedMul α] {a b c : α} : a ≤ b → a ≤ b * c

Alias of le_mul_of_le_left.

theorem le_add_right {α : Type u} [Add α] [Preorder α] [CanonicallyOrderedAdd α] {a b c : α} : a ≤ b → a ≤ b + c

theorem le_mul_self {α : Type u} [CommMagma α] [LE α] [CanonicallyOrderedMul α] {a b : α} : a ≤ b * a

theorem le_add_self {α : Type u} [AddCommMagma α] [LE α] [CanonicallyOrderedAdd α] {a b : α} : a ≤ b + a

@[simp]

theorem self_le_mul_left {α : Type u} [CommMagma α] [LE α] [CanonicallyOrderedMul α] (a b : α) : a ≤ b * a

@[simp]

theorem self_le_add_left {α : Type u} [AddCommMagma α] [LE α] [CanonicallyOrderedAdd α] (a b : α) : a ≤ b + a

theorem le_of_mul_le_right {α : Type u} [CommMagma α] [Preorder α] [CanonicallyOrderedMul α] {a b c : α} : a * b ≤ c → b ≤ c

theorem le_of_add_le_right {α : Type u} [AddCommMagma α] [Preorder α] [CanonicallyOrderedAdd α] {a b c : α} : a + b ≤ c → b ≤ c

theorem le_mul_of_le_right {α : Type u} [CommMagma α] [Preorder α] [CanonicallyOrderedMul α] {a b c : α} : a ≤ c → a ≤ b * c

theorem le_add_of_le_right {α : Type u} [AddCommMagma α] [Preorder α] [CanonicallyOrderedAdd α] {a b c : α} : a ≤ c → a ≤ b + c

theorem le_mul_left {α : Type u} [CommMagma α] [Preorder α] [CanonicallyOrderedMul α] {a b c : α} : a ≤ c → a ≤ b * c

Alias of le_mul_of_le_right.

theorem le_add_left {α : Type u} [AddCommMagma α] [Preorder α] [CanonicallyOrderedAdd α] {a b c : α} : a ≤ c → a ≤ b + c

theorem le_iff_exists_mul' {α : Type u} [CommMagma α] [Preorder α] [CanonicallyOrderedMul α] {a b : α} : a ≤ b ↔ ∃ (c : α), b = c * a

theorem le_iff_exists_add' {α : Type u} [AddCommMagma α] [Preorder α] [CanonicallyOrderedAdd α] {a b : α} : a ≤ b ↔ ∃ (c : α), b = c + a

@[simp]

theorem one_le {α : Type u} [MulOneClass α] [LE α] [CanonicallyOrderedMul α] (a : α) : 1 ≤ a

@[simp]

theorem zero_le {α : Type u} [AddZeroClass α] [LE α] [CanonicallyOrderedAdd α] (a : α) : 0 ≤ a

theorem isBot_one {α : Type u} [MulOneClass α] [LE α] [CanonicallyOrderedMul α] : IsBot 1

theorem isBot_zero {α : Type u} [AddZeroClass α] [LE α] [CanonicallyOrderedAdd α] : IsBot 0

@[simp]

theorem one_lt_of_gt {α : Type u} [MulOneClass α] [Preorder α] [CanonicallyOrderedMul α] {a b : α} (h : a < b) : 1 < b

@[simp]

theorem pos_of_gt {α : Type u} [AddZeroClass α] [Preorder α] [CanonicallyOrderedAdd α] {a b : α} (h : a < b) : 0 < b

theorem LT.lt.pos {α : Type u} [AddZeroClass α] [Preorder α] [CanonicallyOrderedAdd α] {a b : α} (h : a < b) : 0 < b

Alias of pos_of_gt.

theorem LT.lt.one_lt {α : Type u} [MulOneClass α] [Preorder α] [CanonicallyOrderedMul α] {a b : α} (h : a < b) : 1 < b

Alias of one_lt_of_gt.

theorem bot_eq_one {α : Type u} [MulOneClass α] [PartialOrder α] [CanonicallyOrderedMul α] [OrderBot α] : ⊥ = 1

theorem bot_eq_zero {α : Type u} [AddZeroClass α] [PartialOrder α] [CanonicallyOrderedAdd α] [OrderBot α] : ⊥ = 0

@[simp]

theorem le_one_iff_eq_one {α : Type u} [MulOneClass α] [PartialOrder α] [CanonicallyOrderedMul α] {a : α} : a ≤ 1 ↔ a = 1

@[simp]

theorem nonpos_iff_eq_zero {α : Type u} [AddZeroClass α] [PartialOrder α] [CanonicallyOrderedAdd α] {a : α} : a ≤ 0 ↔ a = 0

theorem one_lt_iff_ne_one {α : Type u} [MulOneClass α] [PartialOrder α] [CanonicallyOrderedMul α] {a : α} : 1 < a ↔ a ≠ 1

theorem pos_iff_ne_zero {α : Type u} [AddZeroClass α] [PartialOrder α] [CanonicallyOrderedAdd α] {a : α} : 0 < a ↔ a ≠ 0

theorem one_lt_of_ne_one {α : Type u} [MulOneClass α] [PartialOrder α] [CanonicallyOrderedMul α] {a : α} (h : a ≠ 1) : 1 < a

theorem pos_of_ne_zero {α : Type u} [AddZeroClass α] [PartialOrder α] [CanonicallyOrderedAdd α] {a : α} (h : a ≠ 0) : 0 < a

theorem eq_one_or_one_lt {α : Type u} [MulOneClass α] [PartialOrder α] [CanonicallyOrderedMul α] (a : α) : a = 1 ∨ 1 < a

theorem eq_zero_or_pos {α : Type u} [AddZeroClass α] [PartialOrder α] [CanonicallyOrderedAdd α] (a : α) : a = 0 ∨ 0 < a

theorem one_not_mem_iff {α : Type u} [MulOneClass α] [PartialOrder α] [CanonicallyOrderedMul α] [OrderBot α] {s : Set α} : ¬1 ∈ s ↔ ∀ (x : α), x ∈ s → 1 < x

theorem zero_not_mem_iff {α : Type u} [AddZeroClass α] [PartialOrder α] [CanonicallyOrderedAdd α] [OrderBot α] {s : Set α} : ¬0 ∈ s ↔ ∀ (x : α), x ∈ s → 0 < x

theorem NE.ne.pos {α : Type u} [AddZeroClass α] [PartialOrder α] [CanonicallyOrderedAdd α] {a : α} (h : a ≠ 0) : 0 < a

Alias of pos_of_ne_zero.

theorem NE.ne.one_lt {α : Type u} [MulOneClass α] [PartialOrder α] [CanonicallyOrderedMul α] {a : α} (h : a ≠ 1) : 1 < a

Alias of one_lt_of_ne_one.

theorem exists_one_lt_mul_of_lt {α : Type u} [MulOneClass α] [PartialOrder α] [CanonicallyOrderedMul α] {a b : α} (h : a < b) : ∃ (c : α), ∃ (x : 1 < c), a * c = b

theorem exists_pos_add_of_lt {α : Type u} [AddZeroClass α] [PartialOrder α] [CanonicallyOrderedAdd α] {a b : α} (h : a < b) : ∃ (c : α), ∃ (x : 0 < c), a + c = b

theorem lt_iff_exists_mul {α : Type u} [MulOneClass α] [PartialOrder α] [CanonicallyOrderedMul α] {a b : α} [MulLeftStrictMono α] : a < b ↔ ∃ (c : α), c > 1 ∧ b = a * c

theorem lt_iff_exists_add {α : Type u} [AddZeroClass α] [PartialOrder α] [CanonicallyOrderedAdd α] {a b : α} [AddLeftStrictMono α] : a < b ↔ ∃ (c : α), c > 0 ∧ b = a + c

@[instance 10]

instance CanonicallyOrderedMul.toMulLeftMono {α : Type u} [Semigroup α] [LE α] [CanonicallyOrderedMul α] : MulLeftMono α

@[instance 10]

instance CanonicallyOrderedAdd.toAddLeftMono {α : Type u} [AddSemigroup α] [LE α] [CanonicallyOrderedAdd α] : AddLeftMono α

theorem CanonicallyOrderedMul.toIsOrderedMonoid {α : Type u} [CommMonoid α] [PartialOrder α] [CanonicallyOrderedMul α] : IsOrderedMonoid α

theorem CanonicallyOrderedAdd.toIsOrderedAddMonoid {α : Type u} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] : IsOrderedAddMonoid α

instance CanonicallyOrderedCommMonoid.toUniqueUnits {α : Type u} [Monoid α] [PartialOrder α] [CanonicallyOrderedMul α] : Unique αˣ

Equations

• CanonicallyOrderedCommMonoid.toUniqueUnits = { toInhabited := Units.instInhabited, uniq := ⋯ }

instance CanonicallyOrderedAddCommMonoid.toUniqueAddUnits {α : Type u} [AddMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] : Unique (AddUnits α)

Equations

• CanonicallyOrderedAddCommMonoid.toUniqueAddUnits = { toInhabited := AddUnits.instInhabited, uniq := ⋯ }

@[simp]

theorem one_lt_mul_iff {α : Type u} [CommMonoid α] [PartialOrder α] [CanonicallyOrderedMul α] {a b : α} : 1 < a * b ↔ 1 < a ∨ 1 < b

@[simp]

theorem add_pos_iff {α : Type u} [AddCommMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] {a b : α} : 0 < a + b ↔ 0 < a ∨ 0 < b

theorem NeZero.pos {M : Type u_1} [AddZeroClass M] [PartialOrder M] [CanonicallyOrderedAdd M] (a : M) [NeZero a] : 0 < a

theorem NeZero.of_gt {M : Type u_1} [AddZeroClass M] [Preorder M] [CanonicallyOrderedAdd M] {x y : M} (h : x < y) : NeZero y

@[instance 10]

instance NeZero.of_gt' {M : Type u_1} [AddZeroClass M] [Preorder M] [CanonicallyOrderedAdd M] [One M] {y : M} [Fact (1 < y)] : NeZero y

@[deprecated "Use `[LinearOrderedAddCommMonoid α] [CanonicallyOrderedAdd α]` instead." (since := "2025-01-13")]

structure CanonicallyLinearOrderedAddCommMonoid (α : Type u_1) extends CanonicallyOrderedAddCommMonoid α, LinearOrderedAddCommMonoid α : Type u_1

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

• 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 : α) : AddMonoid.nsmul 0 x = 0
• nsmul_succ (n : ℕ) (x : α) : AddMonoid.nsmul (n + 1) x = AddMonoid.nsmul n 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• 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 (a : α) : ⊥ ≤ a
• exists_add_of_le {a b : α} : a ≤ b → ∃ (c : α), b = a + c
• le_self_add (a b : α) : a ≤ a + b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE α
• toDecidableEq : DecidableEq α
• toDecidableLT : DecidableLT α
• min_def (a b : α) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : α) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b

@[deprecated "Use `[LinearOrderedCommMonoid α] [CanonicallyOrderedMul α]` instead." (since := "2025-01-13")]

structure CanonicallyLinearOrderedCommMonoid (α : Type u_1) extends CanonicallyOrderedCommMonoid α, LinearOrderedCommMonoid α : Type u_1

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

• 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 : α) : Monoid.npow 0 x = 1
• npow_succ (n : ℕ) (x : α) : Monoid.npow (n + 1) x = Monoid.npow n 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 ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le (a b : α) : a < b ↔ a ≤ b ∧ ¬b ≤ a
• 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 (a : α) : ⊥ ≤ a
• exists_mul_of_le {a b : α} : a ≤ b → ∃ (c : α), b = a * c
• le_self_mul (a b : α) : a ≤ a * b
• min : α → α → α
• max : α → α → α
• compare : α → α → Ordering
• le_total (a b : α) : a ≤ b ∨ b ≤ a
• toDecidableLE : DecidableLE α
• toDecidableEq : DecidableEq α
• toDecidableLT : DecidableLT α
• min_def (a b : α) : a ⊓ b = if a ≤ b then a else b
• max_def (a b : α) : a ⊔ b = if a ≤ b then b else a
• compare_eq_compareOfLessAndEq (a b : α) : compare a b = compareOfLessAndEq a b

theorem min_mul_distrib {α : Type u} [CommMonoid α] [LinearOrder α] [CanonicallyOrderedMul α] (a b c : α) : min a (b * c) = min a (min a b * min a c)

theorem min_add_distrib {α : Type u} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] (a b c : α) : min a (b + c) = min a (min a b + min a c)

theorem min_mul_distrib' {α : Type u} [CommMonoid α] [LinearOrder α] [CanonicallyOrderedMul α] (a b c : α) : min (a * b) c = min (min a c * min b c) c

theorem min_add_distrib' {α : Type u} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] (a b c : α) : min (a + b) c = min (min a c + min b c) c

theorem one_min {α : Type u} [CommMonoid α] [LinearOrder α] [CanonicallyOrderedMul α] (a : α) : min 1 a = 1

theorem zero_min {α : Type u} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] (a : α) : min 0 a = 0

theorem min_one {α : Type u} [CommMonoid α] [LinearOrder α] [CanonicallyOrderedMul α] (a : α) : min a 1 = 1

theorem min_zero {α : Type u} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] (a : α) : min a 0 = 0

@[simp]

theorem bot_eq_one' {α : Type u} [CommMonoid α] [LinearOrder α] [CanonicallyOrderedMul α] [OrderBot α] : ⊥ = 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} [AddCommMonoid α] [LinearOrder α] [CanonicallyOrderedAdd α] [OrderBot α] : ⊥ = 0

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