Mathlib.Algebra.Order.Monoid.Canonical.Defs

CanonicallyOrderedAdd structure

(α : Type*) [Add α] [LE α] : Prop
    extends ExistsAddOfLE α

Full source

/-- 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 `OrderedAddCommGroup`s. -/
class CanonicallyOrderedAdd (α : Type*) [Add α] [LE α] : Prop
    extends ExistsAddOfLE α where
  /-- For any `a` and `b`, `a ≤ a + b` -/
  protected le_self_add : ∀ a b : α, a ≤ a + b

Canonically Ordered Additive Monoid

Informal description

An ordered additive monoid $\alpha$ is called *canonically ordered* if the order relation $\leq$ coincides with the subtractibility relation, meaning that $a \leq b$ if and only if there exists an element $c$ such that $b = a + c$. This property is satisfied, for example, by the natural numbers but not by the integers or other nontrivial ordered additive commutative groups.

CanonicallyOrderedMul structure

(α : Type*) [Mul α] [LE α] : Prop
    extends ExistsMulOfLE α

Full source

/-- 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). -/
@[to_additive]
class CanonicallyOrderedMul (α : Type*) [Mul α] [LE α] : Prop
    extends ExistsMulOfLE α where
  /-- For any `a` and `b`, `a ≤ a * b` -/
  protected le_self_mul : ∀ a b : α, a ≤ a * b

Canonically Ordered Multiplicative Monoid

Informal description

A multiplicative monoid $\alpha$ with a preorder $\leq$ is called *canonically ordered* if the ordering coincides with the divisibility relation, meaning that for any elements $a, b \in \alpha$, $a \leq b$ if and only if there exists an element $c \in \alpha$ such that $b = a \cdot c$.

CanonicallyOrderedAddCommMonoid structure

(α : Type*) extends
    OrderedAddCommMonoid α, OrderBot α

Full source

/-- 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 `OrderedAddCommGroup`s. -/
@[deprecated "Use `[OrderedAddCommMonoid α] [CanonicallyOrderedAdd α]` instead."
  (since := "2025-01-13")]
structure CanonicallyOrderedAddCommMonoid (α : Type*) extends
    OrderedAddCommMonoid α, OrderBot α where
  /-- For `a ≤ b`, there is a `c` so `b = a + c`. -/
  protected exists_add_of_le : ∀ {a b : α}, a ≤ b → ∃ c, b = a + c
  /-- For any `a` and `b`, `a ≤ a + b` -/
  protected le_self_add : ∀ a b : α, a ≤ a + b

Canonically Ordered Additive Commutative Monoid

Informal description

A canonically ordered additive commutative monoid is an ordered commutative additive monoid with a bottom element, where the order relation coincides with the subtractibility relation. That is, for any elements $a$ and $b$, $a \leq b$ if and only if there exists an element $c$ such that $b = a + c$. This property is satisfied by structures like the natural numbers but not by ordered additive commutative groups like the integers.

CanonicallyOrderedCommMonoid structure

(α : Type*) extends OrderedCommMonoid α, OrderBot α

Full source

/-- 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).
-/
@[to_additive,
  deprecated "Use `[OrderedCommMonoid α] [CanonicallyOrderedMul α]` instead."
  (since := "2025-01-13")]
structure CanonicallyOrderedCommMonoid (α : Type*) extends OrderedCommMonoid α, OrderBot α where
  /-- For `a ≤ b`, there is a `c` so `b = a * c`. -/
  protected exists_mul_of_le : ∀ {a b : α}, a ≤ b → ∃ c, b = a * c
  /-- For any `a` and `b`, `a ≤ a * b` -/
  protected le_self_mul : ∀ a b : α, a ≤ a * b

Canonically Ordered Commutative Monoid

Informal description

A canonically ordered commutative monoid is an ordered commutative monoid with a least element (order bot) where the ordering coincides with the divisibility relation, meaning that for any elements $a$ and $b$, $a \leq b$ if and only if there exists an element $c$ such that $b = a \cdot c$. This structure combines the properties of an ordered commutative monoid with the existence of a bottom element and the divisibility condition on the order relation.

le_self_mul theorem

: a ≤ a * b

Full source

@[to_additive]
theorem le_self_mul : a ≤ a * b :=
  CanonicallyOrderedMul.le_self_mul _ _

Self-multiplication inequality in canonically ordered monoids: $a \leq a \cdot b$

Informal description

For any elements $a$ and $b$ in a canonically ordered multiplicative monoid $\alpha$, the inequality $a \leq a \cdot b$ holds.

self_le_mul_right theorem

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

Full source

@[to_additive (attr := simp)]
theorem self_le_mul_right (a b : α) : a ≤ a * b :=
  le_self_mul

Self-multiplication inequality in canonically ordered monoids: $a \leq a \cdot b$

Informal description

For any elements $a$ and $b$ in a canonically ordered multiplicative monoid $\alpha$, the inequality $a \leq a \cdot b$ holds.

le_iff_exists_mul theorem

: a ≤ b ↔ ∃ c, b = a * c

Full source

@[to_additive]
theorem le_iff_exists_mul : a ≤ b ↔ ∃ c, b = a * c :=
  ⟨exists_mul_of_le, by
    rintro ⟨c, rfl⟩
    exact le_self_mul⟩

Characterization of Order via Divisibility in Canonically Ordered Monoids

Informal description

For any elements $a$ and $b$ in a canonically ordered multiplicative monoid $\alpha$, the inequality $a \leq b$ holds if and only if there exists an element $c \in \alpha$ such that $b = a \cdot c$.

le_of_mul_le_left theorem

: a * b ≤ c → a ≤ c

Full source

@[to_additive]
theorem le_of_mul_le_left : a * b ≤ c → a ≤ c :=
  le_self_mul.trans

Left Multiplication Implies Inequality in Canonically Ordered Monoids

Informal description

For any elements $a, b, c$ in a canonically ordered multiplicative monoid $\alpha$, if $a \cdot b \leq c$, then $a \leq c$.

le_mul_of_le_left theorem

: a ≤ b → a ≤ b * c

Full source

@[to_additive]
theorem le_mul_of_le_left : a ≤ b → a ≤ b * c :=
  le_self_mul.trans'

Left Multiplication Preserves Order in Canonically Ordered Monoids

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered multiplicative monoid $\alpha$, if $a \leq b$, then $a \leq b \cdot c$.

le_mul_self theorem

: a ≤ b * a

Full source

@[to_additive]
theorem le_mul_self : a ≤ b * a := by
  rw [mul_comm]
  exact le_self_mul

Right Multiplication Inequality in Canonically Ordered Monoids: $a \leq b \cdot a$

Informal description

For any elements $a$ and $b$ in a canonically ordered multiplicative monoid $\alpha$, the inequality $a \leq b \cdot a$ holds.

self_le_mul_left theorem

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

Full source

@[to_additive (attr := simp)]
theorem self_le_mul_left (a b : α) : a ≤ b * a :=
  le_mul_self

Left Multiplication Inequality in Canonically Ordered Monoids: $a \leq b \cdot a$

Informal description

For any elements $a$ and $b$ in a canonically ordered multiplicative monoid $\alpha$, the inequality $a \leq b \cdot a$ holds.

le_of_mul_le_right theorem

: a * b ≤ c → b ≤ c

Full source

@[to_additive]
theorem le_of_mul_le_right : a * b ≤ c → b ≤ c :=
  le_mul_self.trans

Right Factor Order Property in Canonically Ordered Monoids

Informal description

In a canonically ordered multiplicative monoid $\alpha$, for any elements $a, b, c \in \alpha$, if $a \cdot b \leq c$, then $b \leq c$.

le_mul_of_le_right theorem

: a ≤ c → a ≤ b * c

Full source

@[to_additive]
theorem le_mul_of_le_right : a ≤ c → a ≤ b * c :=
  le_mul_self.trans'

Right Multiplication Preserves Order in Canonically Ordered Monoids

Informal description

For any elements $a$, $b$, and $c$ in a canonically ordered multiplicative monoid $\alpha$, if $a \leq c$, then $a \leq b \cdot c$.

le_iff_exists_mul' theorem

: a ≤ b ↔ ∃ c, b = c * a

Full source

@[to_additive]
theorem le_iff_exists_mul' : a ≤ b ↔ ∃ c, b = c * a := by
  simp only [mul_comm _ a, le_iff_exists_mul]

Characterization of Order via Divisibility in Canonically Ordered Monoids

Informal description

For elements $a$ and $b$ in a canonically ordered multiplicative monoid $\alpha$, the inequality $a \leq b$ holds if and only if there exists an element $c \in \alpha$ such that $b = c \cdot a$.

one_le theorem

(a : α) : 1 ≤ a

Full source

@[to_additive (attr := simp) zero_le]
theorem one_le (a : α) : 1 ≤ a :=
  le_self_mul.trans_eq (one_mul _)

One is the Least Element in Canonically Ordered Monoids

Informal description

For any element $a$ in a canonically ordered multiplicative monoid $\alpha$, the inequality $1 \leq a$ holds.

CanonicallyOrderedMul.toOrderBot instance

: OrderBot α

Full source

@[to_additive]
instance (priority := 10) CanonicallyOrderedMul.toOrderBot : OrderBot α where
  bot := 1
  bot_le := one_le

Canonically Ordered Monoids Have Bottom Elements

Informal description

Every canonically ordered multiplicative monoid $\alpha$ has a bottom element $\bot$ with respect to its order.

bot_eq_one theorem

: (⊥ : α) = 1

Full source

@[to_additive] theorem bot_eq_one : (⊥ : α) = 1 := rfl

Bottom Element Equals One in Canonically Ordered Monoids

Informal description

In a canonically ordered multiplicative monoid $\alpha$, the bottom element $\bot$ is equal to the multiplicative identity $1$.

one_lt_of_gt theorem

(h : a < b) : 1 < b

Full source

@[to_additive (attr := simp)]
theorem one_lt_of_gt (h : a < b) : 1 < b :=
  h.bot_lt

Strict Inequality Implies One is Less in Canonically Ordered Monoids

Informal description

For any elements $a$ and $b$ in a canonically ordered multiplicative monoid, if $a < b$, then $1 < b$.

le_one_iff_eq_one theorem

: a ≤ 1 ↔ a = 1

Full source

@[to_additive (attr := simp)] theorem le_one_iff_eq_one : a ≤ 1 ↔ a = 1 := le_bot_iff

Characterization of Multiplicative Identity: $a \leq 1 \leftrightarrow a = 1$

Informal description

For any element $a$ in a canonically ordered multiplicative monoid, $a \leq 1$ if and only if $a = 1$.

one_lt_iff_ne_one theorem

: 1 < a ↔ a ≠ 1

Full source

@[to_additive] theorem one_lt_iff_ne_one : 1 < a ↔ a ≠ 1 := bot_lt_iff_ne_bot

Characterization of Elements Greater Than One in Canonically Ordered Monoids

Informal description

For any element $a$ in a canonically ordered multiplicative monoid, the multiplicative identity $1$ is strictly less than $a$ if and only if $a$ is not equal to $1$, i.e., $1 < a \leftrightarrow a \neq 1$.

one_lt_of_ne_one theorem

(h : a ≠ 1) : 1 < a

Full source

@[to_additive] theorem one_lt_of_ne_one (h : a ≠ 1) : 1 < a := h.bot_lt

Multiplicative Identity is Strictly Less Than Any Non-Identity Element

Informal description

For any element $a$ in a canonically ordered multiplicative monoid, if $a$ is not equal to the multiplicative identity $1$, then $1$ is strictly less than $a$, i.e., $a \neq 1 \implies 1 < a$.

one_not_mem_iff theorem

{s : Set α} : 1 ∉ s ↔ ∀ x ∈ s, 1 < x

Full source

@[to_additive] lemma one_not_mem_iff {s : Set α} : 1 ∉ s1 ∉ s ↔ ∀ x ∈ s, 1 < x := bot_not_mem_iff

Characterization of Sets Excluding the Multiplicative Identity: $1 \notin s \leftrightarrow \forall x \in s, 1 < x$

Informal description

For any subset $s$ of a canonically ordered multiplicative monoid $\alpha$, the multiplicative identity $1$ is not in $s$ if and only if every element $x \in s$ is strictly greater than $1$, i.e., $1 \notin s \leftrightarrow \forall x \in s, 1 < x$.

exists_one_lt_mul_of_lt theorem

(h : a < b) : ∃ (c : _) (_ : 1 < c), a * c = b

Full source

@[to_additive]
theorem exists_one_lt_mul_of_lt (h : a < b) : ∃ (c : _) (_ : 1 < c), a * c = b := by
  obtain ⟨c, hc⟩ := le_iff_exists_mul.1 h.le
  refine ⟨c, one_lt_iff_ne_one.2 ?_, hc.symm⟩
  rintro rfl
  simp [hc, lt_irrefl] at h

Existence of Multiplicative Factor Greater Than One in Strict Inequality for Canonically Ordered Monoids

Informal description

For any elements $a$ and $b$ in a canonically ordered multiplicative monoid $\alpha$, if $a < b$, then there exists an element $c \in \alpha$ such that $1 < c$ and $b = a \cdot c$.

lt_iff_exists_mul theorem

[MulLeftStrictMono α] : a < b ↔ ∃ c > 1, b = a * c

Full source

@[to_additive]
theorem lt_iff_exists_mul [MulLeftStrictMono α] : a < b ↔ ∃ c > 1, b = a * c := by
  rw [lt_iff_le_and_ne, le_iff_exists_mul, ← exists_and_right]
  apply exists_congr
  intro c
  rw [and_comm, and_congr_left_iff, gt_iff_lt]
  rintro rfl
  constructor
  · rw [one_lt_iff_ne_one]
    apply mt
    rintro rfl
    rw [mul_one]
  · rw [← (self_le_mul_right a c).lt_iff_ne]
    apply lt_mul_of_one_lt_right'

Characterization of Strict Order via Multiplicative Factor Greater Than One

Informal description

Let $\alpha$ be a canonically ordered multiplicative monoid with a strictly left-multiplicative monotone operation. For any elements $a, b \in \alpha$, the strict inequality $a < b$ holds if and only if there exists an element $c > 1$ such that $b = a \cdot c$.

CanonicallyOrderedMul.toMulLeftMono instance

: MulLeftMono α

Full source

@[to_additive]
instance (priority := 10) CanonicallyOrderedMul.toMulLeftMono :
    MulLeftMono α where
  elim a b c hbc := by
    obtain ⟨c, hc, rfl⟩ := exists_mul_of_le hbc
    rw [le_iff_exists_mul]
    exact ⟨c, (mul_assoc _ _ _).symm⟩

Left-Multiplicative Monotonicity in Canonically Ordered Monoids

Informal description

Every canonically ordered multiplicative monoid $\alpha$ is left-multiplicative monotone, meaning that for any elements $a, b \in \alpha$, if $a \leq b$, then $c \cdot a \leq c \cdot b$ for all $c \in \alpha$.

CanonicallyOrderedMul.toIsOrderedMonoid theorem

[CommMonoid α] [PartialOrder α] [CanonicallyOrderedMul α] : IsOrderedMonoid α

Full source

@[to_additive]
lemma CanonicallyOrderedMul.toIsOrderedMonoid
    [CommMonoid α] [PartialOrder α] [CanonicallyOrderedMul α] : IsOrderedMonoid α where
  mul_le_mul_left _ _ := mul_le_mul_left'

Canonically Ordered Commutative Monoid is an Ordered Monoid

Informal description

Let $\alpha$ be a commutative monoid with a partial order $\leq$ and the property of being canonically ordered. Then $\alpha$ is an ordered monoid, meaning that the multiplication operation is compatible with the order: for any elements $a, b, c \in \alpha$, if $a \leq b$, then $a \cdot c \leq b \cdot c$ and $c \cdot a \leq c \cdot b$.

CanonicallyOrderedCommMonoid.toUniqueUnits instance

: Unique αˣ

Full source

@[to_additive] instance CanonicallyOrderedCommMonoid.toUniqueUnits : Unique αˣ where
  uniq a := Units.ext <| le_one_iff_eq_one.mp (le_of_mul_le_left a.mul_inv.le)

Trivial Units in Canonically Ordered Commutative Monoids

Informal description

For any canonically ordered commutative monoid $\alpha$, the group of units $\alpha^\times$ is trivial (i.e., contains only the identity element).

one_lt_mul_iff theorem

: 1 < a * b ↔ 1 < a ∨ 1 < b

Full source

@[to_additive (attr := simp) add_pos_iff]
theorem one_lt_mul_iff : 1 < a * b ↔ 1 < a ∨ 1 < b := by
  simp only [one_lt_iff_ne_one, Ne, mul_eq_one, not_and_or]

Product Greater Than One in Canonically Ordered Monoid

Informal description

Let $\alpha$ be a canonically ordered multiplicative monoid. For any elements $a, b \in \alpha$, the product $a \cdot b$ is greater than $1$ if and only if at least one of $a$ or $b$ is greater than $1$.

NeZero.pos theorem

{M} [AddZeroClass M] [PartialOrder M] [CanonicallyOrderedAdd M] (a : M) [NeZero a] : 0 < a

Full source

theorem pos {M} [AddZeroClass M] [PartialOrder M] [CanonicallyOrderedAdd M]
    (a : M) [NeZero a] : 0 < a :=
  (zero_le a).lt_of_ne <| NeZero.out.symm

Nonzero elements are positive in canonically ordered additive monoids

Informal description

Let $M$ be an additively canonically ordered monoid with a partial order and a zero element. For any nonzero element $a \in M$, we have $0 < a$.

NeZero.of_gt theorem

{M} [AddZeroClass M] [Preorder M] [CanonicallyOrderedAdd M] {x y : M} (h : x < y) : NeZero y

Full source

theorem of_gt {M} [AddZeroClass M] [Preorder M] [CanonicallyOrderedAdd M]
    {x y : M} (h : x < y) : NeZero y :=
  of_pos <| pos_of_gt h

Nonzero Elements from Strict Inequality in Canonically Ordered Monoids

Informal description

Let $M$ be an additively canonically ordered monoid with a preorder. For any elements $x, y \in M$ such that $x < y$, the element $y$ is nonzero.

NeZero.of_gt' instance

{M : Type*} [AddZeroClass M] [Preorder M] [CanonicallyOrderedAdd M] [One M] {y : M} [Fact (1 < y)] : NeZero y

Full source

instance (priority := 10) of_gt' {M : Type*} [AddZeroClass M] [Preorder M] [CanonicallyOrderedAdd M]
    [One M] {y : M}
    [Fact (1 < y)] : NeZero y := of_gt <| @Fact.out (1 < y) _

Nonzero Elements from Strict Inequality with One in Canonically Ordered Monoids

Informal description

Let $M$ be an additively canonically ordered monoid with a preorder and a distinguished element $1$. For any element $y \in M$ such that $1 < y$, the element $y$ is nonzero.

CanonicallyLinearOrderedAddCommMonoid structure

(α : Type*)
  extends CanonicallyOrderedAddCommMonoid α, LinearOrderedAddCommMonoid α

Full source

/-- A canonically linear-ordered additive monoid is a canonically ordered additive monoid
    whose ordering is a linear order. -/
@[deprecated "Use `[LinearOrderedAddCommMonoid α] [CanonicallyOrderedAdd α]` instead."
  (since := "2025-01-13")]
structure CanonicallyLinearOrderedAddCommMonoid (α : Type*)
  extends CanonicallyOrderedAddCommMonoid α, LinearOrderedAddCommMonoid α

Canonically linear-ordered additive commutative monoid

Informal description

A canonically linear-ordered additive commutative monoid is a structure that combines the properties of a canonically ordered additive commutative monoid and a linearly ordered additive commutative monoid. This means it is an additive commutative monoid with a linear order where the ordering is compatible with the addition operation, and any element is less than or equal to its sum with another element.

CanonicallyLinearOrderedCommMonoid structure

(α : Type*)
  extends CanonicallyOrderedCommMonoid α, LinearOrderedCommMonoid α

Full source

/-- A canonically linear-ordered monoid is a canonically ordered monoid
    whose ordering is a linear order. -/
@[to_additive,
  deprecated "Use `[LinearOrderedCommMonoid α] [CanonicallyOrderedMul α]` instead."
  (since := "2025-01-13")]
structure CanonicallyLinearOrderedCommMonoid (α : Type*)
  extends CanonicallyOrderedCommMonoid α, LinearOrderedCommMonoid α

Canonically linear-ordered commutative monoid

Informal description

A canonically linear-ordered commutative monoid is a structure that combines the properties of a canonically ordered commutative monoid and a linear-ordered commutative monoid. Specifically, it is a commutative monoid with a linear order where the ordering is compatible with the monoid operation, and every element is greater than or equal to the identity element.

min_mul_distrib theorem

(a b c : α) : min a (b * c) = min a (min a b * min a c)

Full source

@[to_additive]
theorem min_mul_distrib (a b c : α) : min a (b * c) = min a (min a b * min a c) := by
  rcases le_total a b with hb | hb
  · simp [hb, le_mul_right]
  · rcases le_total a c with hc | hc
    · simp [hc, le_mul_left]
    · simp [hb, hc]

Distributivity of Minimum over Multiplication in Canonically Ordered Monoids

Informal description

Let $\alpha$ be a canonically ordered multiplicative monoid. For any elements $a, b, c \in \alpha$, the minimum of $a$ and $b \cdot c$ is equal to the minimum of $a$ and the product of the minima of $a$ with $b$ and $a$ with $c$, i.e., \[ \min(a, b \cdot c) = \min(a, \min(a, b) \cdot \min(a, c)). \]

min_mul_distrib' theorem

(a b c : α) : min (a * b) c = min (min a c * min b c) c

Full source

@[to_additive]
theorem min_mul_distrib' (a b c : α) : min (a * b) c = min (min a c * min b c) c := by
  simpa [min_comm _ c] using min_mul_distrib c a b

Distributivity of Minimum over Multiplication (Dual Form) in Canonically Ordered Monoids

Informal description

Let $\alpha$ be a canonically ordered multiplicative monoid. For any elements $a, b, c \in \alpha$, the minimum of $a \cdot b$ and $c$ is equal to the minimum of the product of the minima of $a$ with $c$ and $b$ with $c$, and $c$ itself, i.e., \[ \min(a \cdot b, c) = \min(\min(a, c) \cdot \min(b, c), c). \]

one_min theorem

(a : α) : min 1 a = 1

Full source

@[to_additive]
theorem one_min (a : α) : min 1 a = 1 :=
  min_eq_left (one_le a)

Minimum with One in Canonically Ordered Monoids

Informal description

For any element $a$ in a canonically ordered multiplicative monoid $\alpha$, the minimum of $1$ and $a$ is equal to $1$, i.e., $\min(1, a) = 1$.

min_one theorem

(a : α) : min a 1 = 1

Full source

@[to_additive]
theorem min_one (a : α) : min a 1 = 1 :=
  min_eq_right (one_le a)

Minimum with One in Canonically Ordered Monoids (Right Form)

Informal description

For any element $a$ in a canonically ordered multiplicative monoid $\alpha$, the minimum of $a$ and $1$ is equal to $1$, i.e., $\min(a, 1) = 1$.

bot_eq_one' theorem

: (⊥ : α) = 1

Full source

/-- In a linearly ordered monoid, we are happy for `bot_eq_one` to be a `@[simp]` lemma. -/
@[to_additive (attr := simp)
  "In a linearly ordered monoid, we are happy for `bot_eq_zero` to be a `@[simp]` lemma"]
theorem bot_eq_one' : (⊥ : α) = 1 :=
  bot_eq_one

Bottom Element Equals One in Canonically Ordered Monoids

Informal description

In a canonically ordered multiplicative monoid $\alpha$, the bottom element $\bot$ is equal to the multiplicative identity $1$, i.e., $\bot = 1$.