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.

We have a ≤ b + a and a ≤ a + b as separate fields. In the commutative case the second field is redundant, but in the noncommutative case (satisfied most relevantly by the ordinals), this extra field allows us to prove more things without the extra commutativity assumption.

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

  For any a and b, a ≤ a + b

• le_self_add (a 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_mul_self (a b : α) : a ≤ b * a

  For any a and b, a ≤ a * b

• le_self_mul (a b : α) : a ≤ a * b

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

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

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_left {α : Type u} [Mul α] [LE α] [CanonicallyOrderedMul α] (a b : α) : a ≤ b * a

@[simp]

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

@[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_of_mul_le_right {α : Type u} [Mul α] [Preorder α] [CanonicallyOrderedMul α] {a b c : α} : a * b ≤ c → b ≤ c

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

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

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

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

Alias of le_mul_of_le_right.

theorem le_add_left {α : Type u} [Add α] [Preorder α] [CanonicallyOrderedAdd α] {a b c : α} : a ≤ c → 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_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

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

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_notMem_iff {α : Type u} [MulOneClass α] [PartialOrder α] [CanonicallyOrderedMul α] [OrderBot α] {s : Set α} : ¬1 ∈ s ↔ ∀ (x : α), x ∈ s → 1 < x

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

@[deprecated zero_notMem_iff (since := "2025-05-23")]

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

Alias of zero_notMem_iff.

@[deprecated one_notMem_iff (since := "2025-05-23")]

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

Alias of one_notMem_iff.

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 CanonicallyOrderedCommMonoid.toUniqueAddUnits {α : Type u} [AddMonoid α] [PartialOrder α] [CanonicallyOrderedAdd α] : Unique (AddUnits α)

Equations

• CanonicallyOrderedCommMonoid.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

theorem NeZero.of_ge {M : Type u_1} [AddZeroClass M] [PartialOrder M] [CanonicallyOrderedAdd M] {x y : M} [NeZero x] (h : x ≤ y) : NeZero y

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

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

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

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

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

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

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

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

@[simp]

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

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