Canonically ordered monoids

class CanonicallyOrderedAddCommMonoid (α : Type u_1) extends OrderedAddCommMonoid , OrderBot , AddCommMonoid , PartialOrder , AddMonoid , AddCommSemigroup , AddSemigroup , AddZeroClass , Zero , AddCommMagma , Add , Preorder , LE , LT , Bot : 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.

theorem CanonicallyOrderedAddCommMonoid.exists_add_of_le {α : Type u_1} [self : CanonicallyOrderedAddCommMonoid α] {a : α} {b : α} : a ≤ b → ∃ (c : α), b = a + c

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

theorem CanonicallyOrderedAddCommMonoid.le_self_add {α : Type u_1} [self : CanonicallyOrderedAddCommMonoid α] (a : α) (b : α) : a ≤ a + b

For any a and b, a ≤ a + b

class CanonicallyOrderedCommMonoid (α : Type u_1) extends OrderedCommMonoid , OrderBot , CommMonoid , PartialOrder , Monoid , CommSemigroup , Semigroup , MulOneClass , One , CommMagma , Mul , Preorder , LE , LT , Bot : 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).

theorem CanonicallyOrderedCommMonoid.exists_mul_of_le {α : Type u_1} [self : CanonicallyOrderedCommMonoid α] {a : α} {b : α} : a ≤ b → ∃ (c : α), b = a * c

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

theorem CanonicallyOrderedCommMonoid.le_self_mul {α : Type u_1} [self : CanonicallyOrderedCommMonoid α] (a : α) (b : α) : a ≤ a * b

For any a and b, a ≤ a * b

@[instance 100]

instance CanonicallyOrderedCommMonoid.existsMulOfLE (α : Type u) [h : CanonicallyOrderedCommMonoid α] : ExistsMulOfLE α

Equations

• ⋯ = ⋯

@[instance 100]

instance CanonicallyOrderedAddCommMonoid.existsAddOfLE (α : Type u) [h : CanonicallyOrderedAddCommMonoid α] : ExistsAddOfLE α

Equations

• ⋯ = ⋯

theorem le_self_mul {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} {c : α} : a ≤ a * c

theorem le_self_add {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} {c : α} : a ≤ a + c

theorem le_mul_self {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} {b : α} : a ≤ b * a

theorem le_add_self {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} {b : α} : a ≤ b + a

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

theorem one_le {α : Type u} [CanonicallyOrderedCommMonoid α] (a : α) : 1 ≤ a

@[simp]

theorem zero_le {α : Type u} [CanonicallyOrderedAddCommMonoid α] (a : α) : 0 ≤ a

theorem bot_eq_one {α : Type u} [CanonicallyOrderedCommMonoid α] : ⊥ = 1

theorem bot_eq_zero {α : Type u} [CanonicallyOrderedAddCommMonoid α] : ⊥ = 0

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

Equations

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

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

Equations

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

@[deprecated mul_eq_one]

theorem mul_eq_one_iff {α : Type u} [CommMonoid α] [Subsingleton αˣ] {a : α} {b : α} : a * b = 1 ↔ a = 1 ∧ b = 1

Alias of mul_eq_one.

@[deprecated add_eq_zero]

theorem add_eq_zero_iff {α : Type u} [AddCommMonoid α] [Subsingleton (AddUnits α)] {a : α} {b : α} : a + b = 0 ↔ a = 0 ∧ b = 0

Alias of add_eq_zero.

@[simp]

theorem le_one_iff_eq_one {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} : a ≤ 1 ↔ a = 1

@[simp]

theorem nonpos_iff_eq_zero {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} : a ≤ 0 ↔ a = 0

theorem one_lt_iff_ne_one {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} : 1 < a ↔ a ≠ 1

theorem pos_iff_ne_zero {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} : 0 < a ↔ a ≠ 0

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

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

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

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

@[simp]

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

@[simp]

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

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

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

theorem le_mul_left {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} {b : α} {c : α} (h : a ≤ c) : a ≤ b * c

theorem le_add_left {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} {b : α} {c : α} (h : a ≤ c) : a ≤ b + c

theorem le_mul_right {α : Type u} [CanonicallyOrderedCommMonoid α] {a : α} {b : α} {c : α} (h : a ≤ b) : a ≤ b * c

theorem le_add_right {α : Type u} [CanonicallyOrderedAddCommMonoid α] {a : α} {b : α} {c : α} (h : a ≤ b) : a ≤ b + c

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

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

theorem pos_of_gt {M : Type u_1} [CanonicallyOrderedAddCommMonoid M] {n : M} {m : M} (h : n < m) : 0 < m

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

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

@[instance 10]

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

Equations

• ⋯ = ⋯

class CanonicallyLinearOrderedAddCommMonoid (α : Type u_1) extends CanonicallyOrderedAddCommMonoid , LinearOrderedAddCommMonoid , OrderedAddCommMonoid , OrderBot , LinearOrder , AddCommMonoid , PartialOrder , AddMonoid , AddCommSemigroup , AddSemigroup , AddZeroClass , Zero , AddCommMagma , Add , Min , Max , Ord , Preorder , LE , LT , Bot : Type u_1

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

class CanonicallyLinearOrderedCommMonoid (α : Type u_1) extends CanonicallyOrderedCommMonoid , LinearOrderedCommMonoid , OrderedCommMonoid , OrderBot , LinearOrder , CommMonoid , PartialOrder , Monoid , CommSemigroup , Semigroup , MulOneClass , One , CommMagma , Mul , Min , Max , Ord , Preorder , LE , LT , Bot : Type u_1

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

@[instance 100]

instance CanonicallyLinearOrderedCommMonoid.semilatticeSup {α : Type u} [CanonicallyLinearOrderedCommMonoid α] : SemilatticeSup α

Equations

• CanonicallyLinearOrderedCommMonoid.semilatticeSup = SemilatticeSup.mk SemilatticeSup.sup ⋯ ⋯ ⋯

@[instance 100]

instance CanonicallyLinearOrderedAddCommMonoid.semilatticeSup {α : Type u} [CanonicallyLinearOrderedAddCommMonoid α] : SemilatticeSup α

Equations

• CanonicallyLinearOrderedAddCommMonoid.semilatticeSup = SemilatticeSup.mk SemilatticeSup.sup ⋯ ⋯ ⋯

theorem min_mul_distrib {α : Type u} [CanonicallyLinearOrderedCommMonoid α] (a : α) (b : α) (c : α) : a ⊓ b * c = a ⊓ (a ⊓ b) * (a ⊓ c)

theorem min_add_distrib {α : Type u} [CanonicallyLinearOrderedAddCommMonoid α] (a : α) (b : α) (c : α) : a ⊓ (b + c) = a ⊓ (a ⊓ b + a ⊓ c)

theorem min_mul_distrib' {α : Type u} [CanonicallyLinearOrderedCommMonoid α] (a : α) (b : α) (c : α) : a * b ⊓ c = (a ⊓ c) * (b ⊓ c) ⊓ c

theorem min_add_distrib' {α : Type u} [CanonicallyLinearOrderedAddCommMonoid α] (a : α) (b : α) (c : α) : (a + b) ⊓ c = (a ⊓ c + b ⊓ c) ⊓ c

theorem one_min {α : Type u} [CanonicallyLinearOrderedCommMonoid α] (a : α) : 1 ⊓ a = 1

theorem zero_min {α : Type u} [CanonicallyLinearOrderedAddCommMonoid α] (a : α) : 0 ⊓ a = 0

theorem min_one {α : Type u} [CanonicallyLinearOrderedCommMonoid α] (a : α) : a ⊓ 1 = 1

theorem min_zero {α : Type u} [CanonicallyLinearOrderedAddCommMonoid α] (a : α) : a ⊓ 0 = 0

@[simp]

theorem bot_eq_one' {α : Type u} [CanonicallyLinearOrderedCommMonoid α] : ⊥ = 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} [CanonicallyLinearOrderedAddCommMonoid α] : ⊥ = 0

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