doc-next-gen

Mathlib.Algebra.Order.Ring.WithTop

Module docstring

{"# Structures involving * and 0 on WithTop and WithBot The main results of this section are WithTop.instOrderedCommSemiring and WithBot.instOrderedCommSemiring. "}

WithTop.instMulZeroClass instance
: MulZeroClass (WithTop α)
Full source 
instance instMulZeroClass : MulZeroClass (WithTop α) where
  zero := 0
  mul
    | (a : α), (b : α) => ↑(a * b)
    | (a : α), ⊤ => if a = 0 then 0 else ⊤
    | ⊤, (b : α) => if b = 0 then 0 else ⊤
    | ⊤, ⊤ => ⊤
  mul_zero
    | (a : α) => congr_arg some <| mul_zero _
    | ⊤ => if_pos rfl
  zero_mul
    | (b : α) => congr_arg some <| zero_mul _
    | ⊤ => if_pos rfl
Multiplication and Zero Structure on `WithTop α`
Informal description
For any type $\alpha$ with a multiplication operation and a zero element, the type `WithTop α` (which adds a top element $\top$ to $\alpha$) inherits a `MulZeroClass` structure. This means that multiplication and zero are extended to `WithTop α` in such a way that $0 \cdot x = 0$ and $x \cdot 0 = 0$ for all $x \in \text{WithTop } \alpha$.
WithTop.coe_mul theorem
(a b : α) : (↑(a * b) : WithTop α) = a * b
Full source 
@[simp, norm_cast] lemma coe_mul (a b : α) : (↑(a * b) : WithTop α) = a * b := rfl
Embedding Preserves Multiplication in $\text{WithTop } \alpha$
Informal description
For any elements $a$ and $b$ of type $\alpha$, the canonical embedding of their product $a * b$ into $\text{WithTop } \alpha$ is equal to the product of their embeddings, i.e., $\uparrow(a * b) = \uparrow a * \uparrow b$.
WithTop.mul_top' theorem
: ∀ (a : WithTop α), a * ⊤ = if a = 0 then 0 else ⊤
Full source 
lemma mul_top' : ∀ (a : WithTop α), a * ⊤ = if a = 0 then 0 else ⊤
  | (a : α) => if_congr coe_eq_zero.symm rfl rfl
  | ⊤ => (if_neg top_ne_zero).symm
Multiplication by Top in $\text{WithTop } \alpha$: $a \cdot \top = \text{if } a = 0 \text{ then } 0 \text{ else } \top$
Informal description
For any element $a$ in $\text{WithTop } \alpha$, the product $a \cdot \top$ equals $0$ if $a = 0$, and equals $\top$ otherwise.
WithTop.mul_top theorem
(h : a ≠ 0) : a * ⊤ = ⊤
Full source 
@[simp] lemma mul_top (h : a ≠ 0) : a * ⊤ = ⊤ := by rw [mul_top', if_neg h]
Multiplication of Nonzero Element by Top Yields Top in $\text{WithTop } \alpha$
Informal description
For any nonzero element $a$ in $\text{WithTop } \alpha$, the product $a \cdot \top$ equals $\top$.
WithTop.top_mul' theorem
: ∀ (b : WithTop α), ⊤ * b = if b = 0 then 0 else ⊤
Full source 
lemma top_mul' : ∀ (b : WithTop α), ⊤ * b = if b = 0 then 0 else ⊤
  | (b : α) => if_congr coe_eq_zero.symm rfl rfl
  | ⊤ => (if_neg top_ne_zero).symm
Top Multiplication Rule in $\text{WithTop } \alpha$: $\top * b = \text{if } b = 0 \text{ then } 0 \text{ else } \top$
Informal description
For any element $b$ in $\text{WithTop } \alpha$ (where $\alpha$ is a type with multiplication and zero), the product of the top element $\top$ and $b$ is defined as: \[ \top * b = \begin{cases} 0 & \text{if } b = 0, \\ \top & \text{otherwise.} \end{cases} \]
WithTop.top_mul theorem
(hb : b ≠ 0) : ⊤ * b = ⊤
Full source 
@[simp] lemma top_mul (hb : b ≠ 0) : ⊤ * b = ⊤ := by rw [top_mul', if_neg hb]
Multiplication of Top with Nonzero Element in $\text{WithTop } \alpha$ Yields Top
Informal description
For any nonzero element $b$ in $\text{WithTop } \alpha$ (where $\alpha$ is a type with multiplication and zero), the product of the top element $\top$ and $b$ is the top element, i.e., $\top * b = \top$.
WithTop.top_mul_top theorem
: (⊤ * ⊤ : WithTop α) = ⊤
Full source 
@[simp] lemma top_mul_top : (⊤ * ⊤ : WithTop α) = ⊤ := rfl
Product of Top Elements in `WithTop α` is Top
Informal description
In the type `WithTop α` (which extends a type $\alpha$ with a top element $\top$), the product of the top element with itself is again the top element, i.e., $\top * \top = \top$.
WithTop.mul_def theorem
(a b : WithTop α) : a * b = if a = 0 ∨ b = 0 then 0 else WithTop.map₂ (· * ·) a b
Full source 
lemma mul_def (a b : WithTop α) :
    a * b = if a = 0 ∨ b = 0 then 0 else WithTop.map₂ (· * ·) a b := by
  cases a <;> cases b <;> aesop
Definition of Multiplication in $\text{WithTop } \alpha$ with Zero Handling
Informal description
For any elements $a$ and $b$ in $\text{WithTop } \alpha$, the product $a * b$ is defined to be $0$ if either $a = 0$ or $b = 0$, and otherwise it is the result of applying the multiplication operation of $\alpha$ pointwise to $a$ and $b$ via $\text{WithTop.map₂}$.
WithTop.mul_eq_top_iff theorem
: a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0
Full source 
lemma mul_eq_top_iff : a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0 := by rw [mul_def]; aesop
Product Equals Top in $\text{WithTop } \alpha$ if and only if One Factor is Top and the Other is Nonzero
Informal description
For any elements $a$ and $b$ in $\text{WithTop } \alpha$, the product $a * b$ equals the top element $\top$ if and only if either $a$ is nonzero and $b$ is $\top$, or $a$ is $\top$ and $b$ is nonzero.
WithTop.mul_coe_eq_bind theorem
{b : α} (hb : b ≠ 0) : ∀ a, (a * b : WithTop α) = a.bind fun a ↦ ↑(a * b)
Full source 
lemma mul_coe_eq_bind {b : α} (hb : b ≠ 0) : ∀ a, (a * b : WithTop α) = a.bind fun a ↦ ↑(a * b)
  | ⊤ => by simp [top_mul, hb]; rfl
  | (a : α) => rfl
Multiplication of Nonzero Element in $\text{WithTop } \alpha$ via Lifting
Informal description
For any nonzero element $b$ in a type $\alpha$ with multiplication and zero, and for any element $a$ in $\text{WithTop } \alpha$, the product $a * b$ (interpreted in $\text{WithTop } \alpha$) is equal to lifting the product $a' * b$ for each $a'$ in $\alpha$ (when $a$ is not $\top$), or $\top$ if $a = \top$.
WithTop.coe_mul_eq_bind theorem
{a : α} (ha : a ≠ 0) : ∀ b, (a * b : WithTop α) = b.bind fun b ↦ ↑(a * b)
Full source 
lemma coe_mul_eq_bind {a : α} (ha : a ≠ 0) : ∀ b, (a * b : WithTop α) = b.bind fun b ↦ ↑(a * b)
  | ⊤ => by simp [top_mul, ha]; rfl
  | (b : α) => rfl
Multiplication of Nonzero Element in $\text{WithTop } \alpha$ via Lifting
Informal description
For any nonzero element $a$ in $\alpha$ and any element $b$ in $\text{WithTop } \alpha$, the product $a * b$ (interpreted in $\text{WithTop } \alpha$) is equal to lifting the product $a * b'$ for each $b'$ in $\alpha$ (when $b$ is not $\top$), or $\top$ if $b = \top$.
WithTop.untopD_zero_mul theorem
(a b : WithTop α) : (a * b).untopD 0 = a.untopD 0 * b.untopD 0
Full source 
@[simp]
lemma untopD_zero_mul (a b : WithTop α) : (a * b).untopD 0 = a.untopD 0 * b.untopD 0 := by
  by_cases ha : a = 0; · rw [ha, zero_mul, ← coe_zero, untopD_coe, zero_mul]
  by_cases hb : b = 0; · rw [hb, mul_zero, ← coe_zero, untopD_coe, mul_zero]
  induction a; · rw [top_mul hb, untopD_top, zero_mul]
  induction b; · rw [mul_top ha, untopD_top, mul_zero]
  rw [← coe_mul, untopD_coe, untopD_coe, untopD_coe]
Default-Untop Operation Preserves Multiplication in $\text{WithTop } \alpha$
Informal description
For any elements $a$ and $b$ in $\text{WithTop } \alpha$, the default-untop operation (with default value $0$) applied to the product $a * b$ equals the product of the default-untop operations applied to $a$ and $b$ individually, i.e., $\text{untopD}(a * b, 0) = \text{untopD}(a, 0) * \text{untopD}(b, 0)$.
WithTop.mul_ne_top theorem
{a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a * b ≠ ⊤
Full source 
theorem mul_ne_top {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a * b ≠ ⊤ := by
  simp [mul_eq_top_iff, *]
Product of Non-Top Elements in $\text{WithTop } \alpha$ is Non-Top
Informal description
For any elements $a$ and $b$ in $\text{WithTop } \alpha$ (where $\alpha$ is a type with multiplication and a zero element), if $a \neq \top$ and $b \neq \top$, then their product $a * b \neq \top$.
WithTop.mul_lt_top theorem
[LT α] {a b : WithTop α} (ha : a < ⊤) (hb : b < ⊤) : a * b < ⊤
Full source 
theorem mul_lt_top [LT α] {a b : WithTop α} (ha : a < ⊤) (hb : b < ⊤) : a * b < ⊤ := by
  rw [WithTop.lt_top_iff_ne_top] at *
  exact mul_ne_top ha hb
Product of Elements Below Top in $\text{WithTop } \alpha$ is Below Top
Informal description
For any type $\alpha$ with a strict order relation $<$, and for any elements $a$ and $b$ in $\text{WithTop } \alpha$ such that $a < \top$ and $b < \top$, their product satisfies $a * b < \top$.
WithTop.instNoZeroDivisors instance
[NoZeroDivisors α] : NoZeroDivisors (WithTop α)
Full source 
instance instNoZeroDivisors [NoZeroDivisors α] : NoZeroDivisors (WithTop α) := by
  refine ⟨fun h₁ => Decidable.byContradiction fun h₂ => ?_⟩
  rw [mul_def, if_neg h₂] at h₁
  rcases Option.mem_map₂_iff.1 h₁ with ⟨a, b, (rfl : _ = _), (rfl : _ = _), hab⟩
  exact h₂ ((eq_zero_or_eq_zero_of_mul_eq_zero hab).imp (congr_arg some) (congr_arg some))
No Zero Divisors in $\text{WithTop } \alpha$
Informal description
For any type $\alpha$ with a multiplication operation and no zero divisors, the type $\text{WithTop } \alpha$ (which adds a top element $\top$ to $\alpha$) also has no zero divisors. This means that for any elements $a$ and $b$ in $\text{WithTop } \alpha$, if $a \cdot b = 0$, then either $a = 0$ or $b = 0$.
WithTop.instMulZeroOneClass instance
[MulZeroOneClass α] [Nontrivial α] : MulZeroOneClass (WithTop α)
Full source 
/-- `Nontrivial α` is needed here as otherwise we have `1 * ⊤ = ⊤` but also `0 * ⊤ = 0`. -/
instance instMulZeroOneClass [MulZeroOneClass α] [Nontrivial α] : MulZeroOneClass (WithTop α) where
  __ := instMulZeroClass
  one_mul
    | ⊤ => mul_top (mt coe_eq_coe.1 one_ne_zero)
    | (a : α) => by rw [← coe_one, ← coe_mul, one_mul]
  mul_one
    | ⊤ => top_mul (mt coe_eq_coe.1 one_ne_zero)
    | (a : α) => by rw [← coe_one, ← coe_mul, mul_one]
Multiplication, Zero, and Identity Structure on $\text{WithTop } \alpha$
Informal description
For any type $\alpha$ with a multiplication operation, a zero element, and a multiplicative identity (i.e., a `MulZeroOneClass` structure), and assuming $\alpha$ is nontrivial (i.e., contains at least two distinct elements), the type $\text{WithTop } \alpha$ (which adds a top element $\top$ to $\alpha$) inherits a `MulZeroOneClass` structure. This means that multiplication, zero, and the multiplicative identity are extended to $\text{WithTop } \alpha$ in such a way that $0 \cdot x = 0$, $x \cdot 0 = 0$, and $1 \cdot x = x$ for all $x \in \text{WithTop } \alpha$.
MonoidWithZeroHom.withTopMap definition
{R S : Type*} [MulZeroOneClass R] [DecidableEq R] [Nontrivial R] [MulZeroOneClass S] [DecidableEq S] [Nontrivial S] (f : R →*₀ S) (hf : Function.Injective f) : WithTop R →*₀ WithTop S
Full source 
/-- A version of `WithTop.map` for `MonoidWithZeroHom`s. -/
@[simps -fullyApplied]
protected def _root_.MonoidWithZeroHom.withTopMap {R S : Type*} [MulZeroOneClass R] [DecidableEq R]
    [Nontrivial R] [MulZeroOneClass S] [DecidableEq S] [Nontrivial S] (f : R →*₀ S)
    (hf : Function.Injective f) : WithTopWithTop R →*₀ WithTop S :=
  { f.toZeroHom.withTopMap, f.toMonoidHom.toOneHom.withTopMap with
    toFun := WithTop.map f
    map_mul' := fun x y => by
      have : ∀ z, mapmap f z = 0 ↔ z = 0 := fun z =>
        (Option.map_injective hf).eq_iff' f.toZeroHom.withTopMap.map_zero
      rcases Decidable.eq_or_ne x 0 with (rfl | hx)
      · simp
      rcases Decidable.eq_or_ne y 0 with (rfl | hy)
      · simp
      induction' x with x
      · simp [hy, this]
      induction' y with y
      · have : (f x : WithTop S) ≠ 0 := by simpa [hf.eq_iff' (map_zero f)] using hx
        simp [mul_top hx, mul_top this]
      · simp [← coe_mul] }
Lifting of monoid with zero homomorphisms to $\text{WithTop}$
Informal description
Given two types $R$ and $S$ each equipped with a multiplication operation, a zero element, and a multiplicative identity (i.e., `MulZeroOneClass` structures), and assuming both are nontrivial and have decidable equality, the function `MonoidWithZeroHom.withTopMap` lifts an injective monoid with zero homomorphism $f : R \to S$ to a monoid with zero homomorphism from $\text{WithTop } R$ to $\text{WithTop } S$. The lifted function maps elements of $R$ via $f$ and preserves the top element $\top$.
WithTop.instSemigroupWithZero instance
[SemigroupWithZero α] [NoZeroDivisors α] : SemigroupWithZero (WithTop α)
Full source 
instance instSemigroupWithZero [SemigroupWithZero α] [NoZeroDivisors α] :
    SemigroupWithZero (WithTop α) where
  __ := instMulZeroClass
  mul_assoc a b c := by
    rcases eq_or_ne a 0 with (rfl | ha); · simp only [zero_mul]
    rcases eq_or_ne b 0 with (rfl | hb); · simp only [zero_mul, mul_zero]
    rcases eq_or_ne c 0 with (rfl | hc); · simp only [mul_zero]
    induction' a with a; · simp [hb, hc]
    induction' b with b; · simp [mul_top ha, top_mul hc]
    induction' c with c
    · rw [mul_top hb, mul_top ha]
      rw [← coe_zero, ne_eq, coe_eq_coe] at ha hb
      simp [ha, hb]
    simp only [← coe_mul, mul_assoc]
Semigroup with Zero Structure on $\text{WithTop } \alpha$
Informal description
For any semigroup with zero $\alpha$ that has no zero divisors, the type $\text{WithTop } \alpha$ (which adds a top element $\top$ to $\alpha$) inherits a semigroup with zero structure. This means that multiplication is associative and satisfies $0 \cdot x = 0$ and $x \cdot 0 = 0$ for all $x \in \text{WithTop } \alpha$.
WithTop.instMonoidWithZero instance
: MonoidWithZero (WithTop α)
Full source 
instance instMonoidWithZero : MonoidWithZero (WithTop α) where
  __ := instMulZeroOneClass
  __ := instSemigroupWithZero
  npow n a := match a, n with
    | (a : α), n => ↑(a ^ n)
    | ⊤, 0 => 1
    | ⊤, _n + 1 => ⊤
  npow_zero a := by cases a <;> simp
  npow_succ n a := by cases n <;> cases a <;> simp [pow_succ]
Monoid with Zero Structure on $\text{WithTop } \alpha$
Informal description
The type $\text{WithTop } \alpha$ (which adds a top element $\top$ to $\alpha$) inherits a monoid with zero structure from $\alpha$. This means that multiplication is associative, has an identity element $1$, and satisfies $0 \cdot x = 0$ and $x \cdot 0 = 0$ for all $x \in \text{WithTop } \alpha$.
WithTop.coe_pow theorem
(a : α) (n : ℕ) : (↑(a ^ n) : WithTop α) = a ^ n
Full source 
@[simp, norm_cast] lemma coe_pow (a : α) (n : ℕ) : (↑(a ^ n) : WithTop α) = a ^ n := rfl
Power Preservation under Canonical Embedding in $\text{WithTop } \alpha$
Informal description
For any element $a$ of type $\alpha$ and any natural number $n$, the canonical embedding of $a^n$ into $\text{WithTop } \alpha$ is equal to the $n$-th power of $a$ in $\text{WithTop } \alpha$, i.e., $\uparrow(a^n) = (\uparrow a)^n$.
WithTop.top_pow theorem
: ∀ {n : ℕ}, n ≠ 0 → (⊤ : WithTop α) ^ n = ⊤
Full source 
@[simp] lemma top_pow : ∀ {n : ℕ}, n ≠ 0 → (⊤ : WithTop α) ^ n = ⊤ | _ + 1, _ => rfl
Top Element Power Identity: $\top^n = \top$ for $n \neq 0$
Informal description
For any natural number $n \neq 0$, the $n$-th power of the top element $\top$ in $\text{WithTop } \alpha$ equals $\top$, i.e., $\top^n = \top$.
WithTop.pow_eq_top_iff theorem
: x ^ n = ⊤ ↔ x = ⊤ ∧ n ≠ 0
Full source 
@[simp] lemma pow_eq_top_iff : x ^ n = ⊤ ↔ x = ⊤ ∧ n ≠ 0 := by
  induction x <;> cases n <;> simp [← coe_pow]
Power Equals Top Condition in $\text{WithTop } \alpha$: $x^n = \top \leftrightarrow x = \top \land n \neq 0$
Informal description
For an element $x \in \text{WithTop } \alpha$ and a natural number $n$, the power $x^n$ equals the top element $\top$ if and only if $x = \top$ and $n \neq 0$. In other words, $x^n = \top \leftrightarrow (x = \top \land n \neq 0)$.
WithTop.pow_ne_top_iff theorem
: x ^ n ≠ ⊤ ↔ x ≠ ⊤ ∨ n = 0
Full source 
lemma pow_ne_top_iff : x ^ n ≠ ⊤x ^ n ≠ ⊤ ↔ x ≠ ⊤ ∨ n = 0 := by simp [pow_eq_top_iff, or_iff_not_imp_left]
Non-top Power Condition in $\text{WithTop } \alpha$: $x^n \neq \top \leftrightarrow x \neq \top \lor n = 0$
Informal description
For an element $x \in \text{WithTop } \alpha$ and a natural number $n$, the power $x^n$ is not equal to $\top$ if and only if either $x \neq \top$ or $n = 0$.
WithTop.pow_lt_top_iff theorem
[Preorder α] : x ^ n < ⊤ ↔ x < ⊤ ∨ n = 0
Full source 
@[simp] lemma pow_lt_top_iff [Preorder α] : x ^ n < ⊤ ↔ x < ⊤ ∨ n = 0 := by
  simp_rw [WithTop.lt_top_iff_ne_top, pow_ne_top_iff]
Power Strictly Less Than Top in $\text{WithTop } \alpha$
Informal description
For a type $\alpha$ with a preorder and an element $x \in \text{WithTop } \alpha$ (where $\text{WithTop } \alpha$ adds a top element $\top$ to $\alpha$), the power $x^n$ is strictly less than $\top$ if and only if either $x$ is strictly less than $\top$ or the exponent $n$ is zero. In other words, $x^n < \top \leftrightarrow x < \top \lor n = 0$.
WithTop.pow_ne_top theorem
(hx : x ≠ ⊤) : x ^ n ≠ ⊤
Full source 
lemma pow_ne_top (hx : x ≠ ⊤) : x ^ n ≠ ⊤ := pow_ne_top_iff.2 <| .inl hx
Non-top Elements Have Non-top Powers in $\text{WithTop } \alpha$
Informal description
For an element $x \in \text{WithTop } \alpha$ (where $\text{WithTop } \alpha$ adds a top element $\top$ to $\alpha$) and a natural number $n$, if $x \neq \top$, then the power $x^n$ is not equal to $\top$.
WithTop.pow_lt_top theorem
[Preorder α] (hx : x < ⊤) : x ^ n < ⊤
Full source 
lemma pow_lt_top [Preorder α] (hx : x < ⊤) : x ^ n < ⊤ := pow_lt_top_iff.2 <| .inl hx
Powers of Non-Top Elements Remain Below Top in $\text{WithTop } \alpha$
Informal description
For an element $x$ in $\text{WithTop } \alpha$ (where $\alpha$ has a preorder) such that $x < \top$, and for any natural number $n$, the power $x^n$ is strictly less than $\top$.
WithTop.instCommMonoidWithZero instance
[CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] : CommMonoidWithZero (WithTop α)
Full source 
instance instCommMonoidWithZero [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] :
    CommMonoidWithZero (WithTop α) where
  __ := instMonoidWithZero
  mul_comm a b := by simp_rw [mul_def]; exact if_congr or_comm rfl (Option.map₂_comm mul_comm)
Commutative Monoid with Zero Structure on $\text{WithTop }\alpha$
Informal description
For any commutative monoid with zero $\alpha$ that has no zero divisors and is nontrivial, the type $\text{WithTop }\alpha$ (which adds a top element $\top$ to $\alpha$) inherits a commutative monoid with zero structure. This means that multiplication is commutative, associative, has an identity element $1$, and satisfies $0 \cdot x = 0$ and $x \cdot 0 = 0$ for all $x \in \text{WithTop }\alpha$.
WithTop.instNonUnitalNonAssocSemiring instance
[NonUnitalNonAssocSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] : NonUnitalNonAssocSemiring (WithTop α)
Full source 
instance instNonUnitalNonAssocSemiring [NonUnitalNonAssocSemiring α] [PartialOrder α]
    [CanonicallyOrderedAdd α] : NonUnitalNonAssocSemiring (WithTop α) where
  toAddCommMonoid := WithTop.addCommMonoid
  __ := WithTop.instMulZeroClass
  right_distrib a b c := by
    induction' c with c
    · by_cases ha : a = 0 <;> simp [ha]
    · by_cases hc : c = 0; · simp [hc]
      simp only [mul_coe_eq_bind hc]
      cases a <;> cases b <;> try rfl
      exact congr_arg some (add_mul _ _ _)
  left_distrib c a b := by
    induction' c with c
    · by_cases ha : a = 0 <;> simp [ha]
    · by_cases hc : c = 0; · simp [hc]
      simp only [coe_mul_eq_bind hc]
      cases a <;> cases b <;> try rfl
      exact congr_arg some (mul_add _ _ _)
Non-Unital Non-Associative Semiring Structure on $\text{WithTop }\alpha$
Informal description
For any type $\alpha$ with a non-unital non-associative semiring structure, a partial order, and a canonically ordered additive monoid structure, the type $\text{WithTop }\alpha$ (which adds a top element $\top$ to $\alpha$) inherits a non-unital non-associative semiring structure. This means that addition and multiplication are extended to $\text{WithTop }\alpha$ in a way that preserves the semiring properties, while not requiring the existence of a multiplicative identity or associativity of multiplication.
WithTop.instNonAssocSemiring instance
[NonAssocSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [Nontrivial α] : NonAssocSemiring (WithTop α)
Full source 
instance instNonAssocSemiring [NonAssocSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α]
    [Nontrivial α] : NonAssocSemiring (WithTop α) where
  toNonUnitalNonAssocSemiring := instNonUnitalNonAssocSemiring
  __ := WithTop.instMulZeroOneClass
  __ := WithTop.addCommMonoidWithOne
Non-Associative Semiring Structure on $\text{WithTop }\alpha$
Informal description
For any type $\alpha$ with a non-associative semiring structure, a partial order, and a canonically ordered additive monoid structure, and assuming $\alpha$ is nontrivial, the type $\text{WithTop }\alpha$ (which adds a top element $\top$ to $\alpha$) inherits a non-associative semiring structure. This means that addition and multiplication are extended to $\text{WithTop }\alpha$ in a way that preserves the semiring properties, while not requiring the associativity of multiplication.
WithTop.instNonUnitalSemiring instance
[NonUnitalSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] : NonUnitalSemiring (WithTop α)
Full source 
instance instNonUnitalSemiring [NonUnitalSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α]
    [NoZeroDivisors α] : NonUnitalSemiring (WithTop α) where
  toNonUnitalNonAssocSemiring := WithTop.instNonUnitalNonAssocSemiring
  __ := WithTop.instSemigroupWithZero
Non-Unital Semiring Structure on $\text{WithTop }\alpha$
Informal description
For any non-unital semiring $\alpha$ with a partial order and canonically ordered additive monoid structure, and with no zero divisors, the type $\text{WithTop }\alpha$ (which adds a top element $\top$ to $\alpha$) inherits a non-unital semiring structure. This means that addition and multiplication are extended to $\text{WithTop }\alpha$ in a way that preserves the semiring properties, while not requiring the existence of a multiplicative identity.
WithTop.instSemiring instance
[Semiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] : Semiring (WithTop α)
Full source 
instance instSemiring [Semiring α] [PartialOrder α] [CanonicallyOrderedAdd α]
    [NoZeroDivisors α] [Nontrivial α] : Semiring (WithTop α) where
  toNonUnitalSemiring := WithTop.instNonUnitalSemiring
  __ := WithTop.instMonoidWithZero
  __ := WithTop.addCommMonoidWithOne
Semiring Structure on $\text{WithTop }\alpha$
Informal description
For any semiring $\alpha$ with a partial order, canonically ordered additive monoid structure, no zero divisors, and nontrivial structure, the type $\text{WithTop }\alpha$ (which adds a top element $\top$ to $\alpha$) inherits a semiring structure. This means that addition and multiplication are extended to $\text{WithTop }\alpha$ in a way that preserves the semiring properties, including associativity and distributivity of multiplication over addition, and the existence of a multiplicative identity.
WithTop.instCommSemiring instance
[CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] : CommSemiring (WithTop α)
Full source 
instance instCommSemiring [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α]
    [NoZeroDivisors α] [Nontrivial α] : CommSemiring (WithTop α) where
  toSemiring := WithTop.instSemiring
  __ := WithTop.instCommMonoidWithZero
Commutative Semiring Structure on $\text{WithTop }\alpha$
Informal description
For any commutative semiring $\alpha$ with a partial order, canonically ordered additive monoid structure, no zero divisors, and nontrivial structure, the type $\text{WithTop }\alpha$ (which adds a top element $\top$ to $\alpha$) inherits a commutative semiring structure. This means that addition and multiplication are extended to $\text{WithTop }\alpha$ in a way that preserves the semiring properties, including commutativity, associativity, and distributivity of multiplication over addition, and the existence of a multiplicative identity.
WithTop.instIsOrderedRing instance
[CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] : IsOrderedRing (WithTop α)
Full source 
instance instIsOrderedRing [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α]
    [NoZeroDivisors α] [Nontrivial α] : IsOrderedRing (WithTop α) :=
  CanonicallyOrderedAdd.toIsOrderedRing
Ordered Ring Structure on $\text{WithTop }\alpha$
Informal description
For any commutative semiring $\alpha$ with a partial order, canonically ordered additive monoid structure, no zero divisors, and nontrivial structure, the type $\text{WithTop }\alpha$ (which adds a top element $\top$ to $\alpha$) inherits an ordered ring structure. This means that the multiplication and addition operations on $\text{WithTop }\alpha$ preserve the order relation, and the ring axioms hold in this extended setting.
RingHom.withTopMap definition
{R S : Type*} [NonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [DecidableEq R] [Nontrivial R] [NonAssocSemiring S] [PartialOrder S] [CanonicallyOrderedAdd S] [DecidableEq S] [Nontrivial S] (f : R →+* S) (hf : Function.Injective f) : WithTop R →+* WithTop S
Full source 
/-- A version of `WithTop.map` for `RingHom`s. -/
@[simps -fullyApplied]
protected def _root_.RingHom.withTopMap {R S : Type*}
    [NonAssocSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R]
    [DecidableEq R] [Nontrivial R]
    [NonAssocSemiring S] [PartialOrder S] [CanonicallyOrderedAdd S]
    [DecidableEq S] [Nontrivial S]
    (f : R →+* S) (hf : Function.Injective f) : WithTopWithTop R →+* WithTop S :=
  {MonoidWithZeroHom.withTopMap f.toMonoidWithZeroHom hf, f.toAddMonoidHom.withTopMap with}
Lifting of ring homomorphisms to $\text{WithTop}$
Informal description
Given two non-associative semirings $R$ and $S$ with partial orders and canonically ordered additive structures, and assuming both are nontrivial and have decidable equality, the function `RingHom.withTopMap` lifts an injective ring homomorphism $f : R \to S$ to a ring homomorphism from $\text{WithTop } R$ to $\text{WithTop } S$. The lifted function maps elements of $R$ via $f$ and preserves the top element $\top$.
WithTop.mul_lt_mul theorem
(ha : a₁ < a₂) (hb : b₁ < b₂) : a₁ * b₁ < a₂ * b₂
Full source 
@[gcongr]
protected lemma mul_lt_mul (ha : a₁ < a₂) (hb : b₁ < b₂) : a₁ * b₁ < a₂ * b₂ := by
  have := posMulStrictMono_iff_mulPosStrictMono.1 ‹_›
  lift a₁ to α using ha.lt_top.ne
  lift b₁ to α using hb.lt_top.ne
  obtain rfl | ha₂ := eq_or_ne a₂ ⊤
  · rw [top_mul (by simpa [bot_eq_zero] using hb.bot_lt.ne')]
    exact coe_lt_top _
  obtain rfl | hb₂ := eq_or_ne b₂ ⊤
  · rw [mul_top (by simpa [bot_eq_zero] using ha.bot_lt.ne')]
    exact coe_lt_top _
  lift a₂ to α using ha₂
  lift b₂ to α using hb₂
  norm_cast at *
  obtain rfl | hb₁ := eq_zero_or_pos b₁
  · rw [mul_zero]
    exact mul_pos (by simpa [bot_eq_zero] using ha.bot_lt) hb
  · exact mul_lt_mul ha hb.le hb₁ (zero_le _)
Strict Monotonicity of Multiplication in $\text{WithTop } \alpha$
Informal description
For any elements $a_1, a_2, b_1, b_2$ in $\text{WithTop } \alpha$, if $a_1 < a_2$ and $b_1 < b_2$, then $a_1 \cdot b_1 < a_2 \cdot b_2$.
WithTop.pow_right_strictMono theorem
: ∀ {n : ℕ}, n ≠ 0 → StrictMono fun a : WithTop α ↦ a ^ n
Full source 
protected lemma pow_right_strictMono : ∀ {n : ℕ}, n ≠ 0 → StrictMono fun a : WithTop α ↦ a ^ n
  | 0, h => absurd rfl h
  | 1, _ => by simpa only [pow_one] using strictMono_id
  | n + 2, _ => fun x y h ↦ by
    simp_rw [pow_succ _ (n + 1)]
    exact WithTop.mul_lt_mul (WithTop.pow_right_strictMono n.succ_ne_zero h) h
Strict Monotonicity of Power Function on $\text{WithTop } \alpha$ for Nonzero Exponents
Informal description
For any natural number $n \neq 0$, the function $a \mapsto a^n$ is strictly monotone on $\text{WithTop } \alpha$, where $\text{WithTop } \alpha$ is the type obtained by adjoining a top element $\top$ to $\alpha$.
WithTop.pow_lt_pow_left theorem
(hab : a < b) {n : ℕ} (hn : n ≠ 0) : a ^ n < b ^ n
Full source 
@[gcongr] protected lemma pow_lt_pow_left (hab : a < b) {n : ℕ} (hn : n ≠ 0) : a ^ n < b ^ n :=
  WithTop.pow_right_strictMono hn hab
Strict Monotonicity of Powers in $\text{WithTop } \alpha$ for Nonzero Exponents
Informal description
For any elements $a$ and $b$ in $\text{WithTop } \alpha$ such that $a < b$, and for any natural number $n \neq 0$, we have $a^n < b^n$.
WithBot.instMulZeroClass instance
: MulZeroClass (WithBot α)
Full source 
instance : MulZeroClass (WithBot α) := WithTop.instMulZeroClass
Multiplication and Zero Structure on `WithBot α`
Informal description
For any type $\alpha$ with a multiplication operation and a zero element, the type `WithBot α` (which adds a bottom element $\bot$ to $\alpha$) inherits a `MulZeroClass` structure. This means that multiplication and zero are extended to `WithBot α` in such a way that $0 \cdot x = 0$ and $x \cdot 0 = 0$ for all $x \in \text{WithBot } \alpha$.
WithBot.coe_mul theorem
(a b : α) : (↑(a * b) : WithBot α) = a * b
Full source 
@[simp, norm_cast] lemma coe_mul (a b : α) : (↑(a * b) : WithBot α) = a * b := rfl
Embedding Preserves Multiplication in $\text{WithBot } \alpha$
Informal description
For any elements $a$ and $b$ in a type $\alpha$, the canonical embedding of their product $a * b$ into $\text{WithBot } \alpha$ is equal to the product of their embeddings, i.e., $\uparrow(a * b) = \uparrow a * \uparrow b$.
WithBot.mul_bot' theorem
: ∀ (a : WithBot α), a * ⊥ = if a = 0 then 0 else ⊥
Full source 
lemma mul_bot' : ∀ (a : WithBot α), a * ⊥ = if a = 0 then 0 else ⊥
  | (a : α) => if_congr coe_eq_zero.symm rfl rfl
  | ⊥ => (if_neg bot_ne_zero).symm
Multiplication with Bottom Element in $\text{WithBot } \alpha$: $a \cdot \bot = \text{if } a = 0 \text{ then } 0 \text{ else } \bot$
Informal description
For any element $a$ in $\text{WithBot } \alpha$, the product $a \cdot \bot$ is equal to $0$ if $a = 0$, and $\bot$ otherwise.
WithBot.mul_bot theorem
(h : a ≠ 0) : a * ⊥ = ⊥
Full source 
@[simp] lemma mul_bot (h : a ≠ 0) : a * ⊥ = ⊥ := by rw [mul_bot', if_neg h]
Nonzero Multiplication with Bottom Element in $\text{WithBot } \alpha$: $a \cdot \bot = \bot$ for $a \neq 0$
Informal description
For any element $a$ in $\text{WithBot } \alpha$ such that $a \neq 0$, the product $a \cdot \bot$ is equal to $\bot$.
WithBot.bot_mul' theorem
: ∀ (b : WithBot α), ⊥ * b = if b = 0 then 0 else ⊥
Full source 
lemma bot_mul' : ∀ (b : WithBot α), ⊥ * b = if b = 0 then 0 else ⊥
  | (b : α) => if_congr coe_eq_zero.symm rfl rfl
  | ⊥ => (if_neg bot_ne_zero).symm
Left Multiplication by Bottom Element in $\text{WithBot } \alpha$: $\bot \cdot b = \text{if } b = 0 \text{ then } 0 \text{ else } \bot$
Informal description
For any element $b$ in $\text{WithBot } \alpha$, the product $\bot \cdot b$ is equal to $0$ if $b = 0$, and $\bot$ otherwise.
WithBot.bot_mul theorem
(hb : b ≠ 0) : ⊥ * b = ⊥
Full source 
@[simp] lemma bot_mul (hb : b ≠ 0) : ⊥ * b = ⊥ := by rw [bot_mul', if_neg hb]
Left Multiplication by Bottom Element in $\text{WithBot } \alpha$ for Nonzero $b$: $\bot \cdot b = \bot$
Informal description
For any element $b$ in $\text{WithBot } \alpha$ such that $b \neq 0$, the product $\bot \cdot b$ is equal to $\bot$.
WithBot.bot_mul_bot theorem
: (⊥ * ⊥ : WithBot α) = ⊥
Full source 
@[simp] lemma bot_mul_bot : (⊥ * ⊥ : WithBot α) = ⊥ := rfl
Product of Bottom Elements in `WithBot α`
Informal description
In the type `WithBot α` (which extends a type `α` with a bottom element $\bot$), the product of two bottom elements is equal to the bottom element, i.e., $\bot * \bot = \bot$.
WithBot.mul_def theorem
(a b : WithBot α) : a * b = if a = 0 ∨ b = 0 then 0 else WithBot.map₂ (· * ·) a b
Full source 
lemma mul_def (a b : WithBot α) :
    a * b = if a = 0 ∨ b = 0 then 0 else WithBot.map₂ (· * ·) a b := by
  cases a <;> cases b <;> aesop
Definition of Multiplication in $\text{WithBot } \alpha$: $a \cdot b = 0$ if either is zero, else lifted multiplication
Informal description
For any elements $a$ and $b$ in $\text{WithBot } \alpha$, the product $a \cdot b$ is defined as follows: if either $a = 0$ or $b = 0$, then $a \cdot b = 0$; otherwise, $a \cdot b$ is the result of lifting the multiplication operation from $\alpha$ to $\text{WithBot } \alpha$ via $\text{WithBot.map₂}$.
WithBot.mul_eq_bot_iff theorem
: a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0
Full source 
lemma mul_eq_bot_iff : a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0 := by rw [mul_def]; aesop
Product Equals Bottom in $\text{WithBot } \alpha$ if and only if One Factor is Bottom and the Other is Nonzero
Informal description
For any elements $a$ and $b$ in $\text{WithBot } \alpha$, the product $a \cdot b$ equals the bottom element $\bot$ if and only if either $a$ is nonzero and $b$ is $\bot$, or $a$ is $\bot$ and $b$ is nonzero.
WithBot.mul_coe_eq_bind theorem
{b : α} (hb : b ≠ 0) : ∀ a, (a * b : WithBot α) = a.bind fun a ↦ ↑(a * b)
Full source 
lemma mul_coe_eq_bind {b : α} (hb : b ≠ 0) : ∀ a, (a * b : WithBot α) = a.bind fun a ↦ ↑(a * b)
  | ⊥ => by simp only [ne_eq, coe_eq_zero, hb, not_false_eq_true, bot_mul]; rfl
  | (a : α) => rfl
Multiplication of Nonzero Element with $\text{WithBot}$ Element via Lifting
Informal description
For any nonzero element $b$ in a type $\alpha$ with multiplication and zero, and for any element $a$ in $\text{WithBot } \alpha$, the product $a \cdot b$ in $\text{WithBot } \alpha$ is equal to the result of applying the function $\lambda a', \uparrow (a' \cdot b)$ to $a$ (where $\uparrow$ denotes the coercion from $\alpha$ to $\text{WithBot } \alpha$). More precisely, if $a = \uparrow a'$ for some $a' \in \alpha$, then $a \cdot b = \uparrow (a' \cdot b)$; if $a = \bot$, then $a \cdot b = \bot$.
WithBot.coe_mul_eq_bind theorem
{a : α} (ha : a ≠ 0) : ∀ b, (a * b : WithBot α) = b.bind fun b ↦ ↑(a * b)
Full source 
lemma coe_mul_eq_bind {a : α} (ha : a ≠ 0) : ∀ b, (a * b : WithBot α) = b.bind fun b ↦ ↑(a * b)
  | ⊥ => by simp only [ne_eq, coe_eq_zero, ha, not_false_eq_true, mul_bot]; rfl
  | (b : α) => rfl
Multiplication of Nonzero Element with $\text{WithBot}$ Element via Lifting
Informal description
For any nonzero element $a \in \alpha$ and any element $b \in \text{WithBot } \alpha$, the product $a * b$ in $\text{WithBot } \alpha$ is equal to lifting the product $a * b'$ for each $b' \in \alpha$ obtained from $b$ (or $\bot$ if $b = \bot$). More precisely, if $a \neq 0$, then for any $b \in \text{WithBot } \alpha$, we have: $$ a * b = \begin{cases} \uparrow (a * b') & \text{if } b = \uparrow b' \\ \bot & \text{if } b = \bot \end{cases} $$ where $\uparrow$ denotes the coercion from $\alpha$ to $\text{WithBot } \alpha$.
WithBot.unbotD_zero_mul theorem
(a b : WithBot α) : (a * b).unbotD 0 = a.unbotD 0 * b.unbotD 0
Full source 
@[simp]
lemma unbotD_zero_mul (a b : WithBot α) : (a * b).unbotD 0 = a.unbotD 0 * b.unbotD 0 := by
  by_cases ha : a = 0; · rw [ha, zero_mul, ← coe_zero, unbotD_coe, zero_mul]
  by_cases hb : b = 0; · rw [hb, mul_zero, ← coe_zero, unbotD_coe, mul_zero]
  induction a; · rw [bot_mul hb, unbotD_bot, zero_mul]
  induction b; · rw [mul_bot ha, unbotD_bot, mul_zero]
  rw [← coe_mul, unbotD_coe, unbotD_coe, unbotD_coe]
Default Value of Product in $\text{WithBot } \alpha$ Equals Product of Default Values
Informal description
For any elements $a$ and $b$ in $\text{WithBot } \alpha$, the default value of the product $a * b$ (with $\bot$ mapped to $0$) is equal to the product of the default values of $a$ and $b$ (each with $\bot$ mapped to $0$). In other words, $(a * b).\text{unbotD } 0 = a.\text{unbotD } 0 * b.\text{unbotD } 0$.
WithBot.mul_ne_bot theorem
{a b : WithBot α} (ha : a ≠ ⊥) (hb : b ≠ ⊥) : a * b ≠ ⊥
Full source 
theorem mul_ne_bot {a b : WithBot α} (ha : a ≠ ⊥) (hb : b ≠ ⊥) : a * b ≠ ⊥ :=
  WithTop.mul_ne_top (α := αᵒᵈ) ha hb
Product of Non-Bottom Elements in $\text{WithBot } \alpha$ is Non-Bottom
Informal description
For any elements $a$ and $b$ in $\text{WithBot } \alpha$ (where $\alpha$ is a type with multiplication and a zero element), if $a \neq \bot$ and $b \neq \bot$, then their product $a * b \neq \bot$.
WithBot.bot_lt_mul theorem
[LT α] {a b : WithBot α} (ha : ⊥ < a) (hb : ⊥ < b) : ⊥ < a * b
Full source 
theorem bot_lt_mul [LT α] {a b : WithBot α} (ha : ⊥ < a) (hb : ⊥ < b) : ⊥ < a * b :=
  WithTop.mul_lt_top (α := αᵒᵈ) ha hb
Product of Elements Above Bottom in $\text{WithBot } \alpha$ is Above Bottom
Informal description
For any type $\alpha$ with a strict order relation $<$, and for any elements $a$ and $b$ in $\text{WithBot } \alpha$ such that $\bot < a$ and $\bot < b$, their product satisfies $\bot < a * b$.
WithBot.instNoZeroDivisors instance
[NoZeroDivisors α] : NoZeroDivisors (WithBot α)
Full source 
instance instNoZeroDivisors [NoZeroDivisors α] : NoZeroDivisors (WithBot α) :=
  WithTop.instNoZeroDivisors
No Zero Divisors in $\text{WithBot } \alpha$
Informal description
For any type $\alpha$ with no zero divisors, the type $\text{WithBot } \alpha$ (obtained by adjoining a bottom element $\bot$ to $\alpha$) also has no zero divisors. That is, if $a \cdot b = 0$ for $a, b \in \text{WithBot } \alpha$, then either $a = 0$ or $b = 0$.
WithBot.instMulZeroOneClass instance
[MulZeroOneClass α] [Nontrivial α] : MulZeroOneClass (WithBot α)
Full source 
/-- `Nontrivial α` is needed here as otherwise we have `1 * ⊥ = ⊥` but also `= 0 * ⊥ = 0`. -/
instance instMulZeroOneClass [MulZeroOneClass α] [Nontrivial α] : MulZeroOneClass (WithBot α) :=
  WithTop.instMulZeroOneClass
Multiplication, Zero, and Identity Structure on $\text{WithBot } \alpha$
Informal description
For any type $\alpha$ with a multiplication operation, a zero element, and a multiplicative identity (i.e., a `MulZeroOneClass` structure), and assuming $\alpha$ is nontrivial (i.e., contains at least two distinct elements), the type $\text{WithBot } \alpha$ (which adds a bottom element $\bot$ to $\alpha$) inherits a `MulZeroOneClass` structure. This means that multiplication, zero, and the multiplicative identity are extended to $\text{WithBot } \alpha$ in such a way that $0 \cdot x = 0$, $x \cdot 0 = 0$, and $1 \cdot x = x$ for all $x \in \text{WithBot } \alpha$.
WithBot.instSemigroupWithZero instance
[SemigroupWithZero α] [NoZeroDivisors α] : SemigroupWithZero (WithBot α)
Full source 
instance instSemigroupWithZero [SemigroupWithZero α] [NoZeroDivisors α] :
    SemigroupWithZero (WithBot α) := WithTop.instSemigroupWithZero
Semigroup with Zero Structure on $\text{WithBot } \alpha$
Informal description
For any semigroup with zero $\alpha$ that has no zero divisors, the type $\text{WithBot } \alpha$ (which adds a bottom element $\bot$ to $\alpha$) inherits a semigroup with zero structure. This means that multiplication is associative and satisfies $0 \cdot x = 0$ and $x \cdot 0 = 0$ for all $x \in \text{WithBot } \alpha$.
WithBot.instMonoidWithZero instance
: MonoidWithZero (WithBot α)
Full source 
instance instMonoidWithZero : MonoidWithZero (WithBot α) := WithTop.instMonoidWithZero
Monoid with Zero Structure on $\text{WithBot } \alpha$
Informal description
The type $\text{WithBot } \alpha$ (which adds a bottom element $\bot$ to $\alpha$) inherits a monoid with zero structure from $\alpha$. This means that multiplication is associative, has an identity element $1$, and satisfies $0 \cdot x = 0$ and $x \cdot 0 = 0$ for all $x \in \text{WithBot } \alpha$.
WithBot.coe_pow theorem
(a : α) (n : ℕ) : (↑(a ^ n) : WithBot α) = a ^ n
Full source 
@[simp, norm_cast] lemma coe_pow (a : α) (n : ℕ) : (↑(a ^ n) : WithBot α) = a ^ n := rfl
Preservation of Powers under Canonical Embedding in $\text{WithBot } \alpha$
Informal description
For any element $a$ of type $\alpha$ and any natural number $n$, the canonical embedding of $a^n$ into $\text{WithBot } \alpha$ is equal to $a$ raised to the power $n$ in $\text{WithBot } \alpha$, i.e., $\uparrow(a^n) = a^n$.
WithBot.instCommMonoidWithZero instance
[CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] : CommMonoidWithZero (WithBot α)
Full source 
instance instCommMonoidWithZero [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] :
    CommMonoidWithZero (WithBot α) :=
  WithTop.instCommMonoidWithZero
Commutative Monoid with Zero Structure on $\text{WithBot }\alpha$
Informal description
For any commutative monoid with zero $\alpha$ that has no zero divisors and is nontrivial, the type $\text{WithBot }\alpha$ (which adds a bottom element $\bot$ to $\alpha$) inherits a commutative monoid with zero structure. This means that multiplication is commutative, associative, has an identity element $1$, and satisfies $0 \cdot x = 0$ and $x \cdot 0 = 0$ for all $x \in \text{WithBot }\alpha$.
WithBot.instCommSemiring instance
[CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] : CommSemiring (WithBot α)
Full source 
instance instCommSemiring [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α]
    [NoZeroDivisors α] [Nontrivial α] :
    CommSemiring (WithBot α) :=
  WithTop.instCommSemiring
Commutative Semiring Structure on $\text{WithBot }\alpha$
Informal description
For any commutative semiring $\alpha$ with a partial order, canonically ordered additive monoid structure, no zero divisors, and nontrivial structure, the type $\text{WithBot }\alpha$ (which adds a bottom element $\bot$ to $\alpha$) inherits a commutative semiring structure. This means that addition and multiplication are extended to $\text{WithBot }\alpha$ in a way that preserves the semiring properties, including commutativity, associativity, and distributivity of multiplication over addition, and the existence of a multiplicative identity.
WithBot.instPosMulMono instance
[MulZeroClass α] [Preorder α] [PosMulMono α] : PosMulMono (WithBot α)
Full source 
instance [MulZeroClass α] [Preorder α] [PosMulMono α] : PosMulMono (WithBot α) where
  elim := by
    intro ⟨x, x0⟩ a b h
    simp only [Subtype.coe_mk]
    rcases eq_or_ne x 0 with rfl | x0'
    · simp
    lift x to α
    · rintro rfl
      exact (WithBot.bot_lt_coe (0 : α)).not_le x0
    induction a
    · simp_rw [mul_bot x0', bot_le]
    induction b
    · exact absurd h (bot_lt_coe _).not_le
    simp only [← coe_mul, coe_le_coe] at *
    norm_cast at x0
    exact mul_le_mul_of_nonneg_left h x0
Monotonicity of Left Multiplication by Nonnegative Elements in `WithBot α`
Informal description
For any type $\alpha$ with a multiplication operation, a zero element, and a preorder such that left multiplication by nonnegative elements is monotone, the type `WithBot α` (which adds a bottom element $\bot$ to $\alpha$) also satisfies the property that left multiplication by nonnegative elements is monotone.
WithBot.instMulPosMono instance
[MulZeroClass α] [Preorder α] [MulPosMono α] : MulPosMono (WithBot α)
Full source 
instance [MulZeroClass α] [Preorder α] [MulPosMono α] : MulPosMono (WithBot α) where
  elim := by
    intro ⟨x, x0⟩ a b h
    simp only [Subtype.coe_mk]
    rcases eq_or_ne x 0 with rfl | x0'
    · simp
    lift x to α
    · rintro rfl
      exact (WithBot.bot_lt_coe (0 : α)).not_le x0
    induction a
    · simp_rw [bot_mul x0', bot_le]
    induction b
    · exact absurd h (bot_lt_coe _).not_le
    simp only [← coe_mul, coe_le_coe] at *
    norm_cast at x0
    exact mul_le_mul_of_nonneg_right h x0
Monotonicity of Right Multiplication by Nonnegative Elements in $\text{WithBot } \alpha$
Informal description
For any type $\alpha$ with a multiplication operation, a zero element, and a preorder such that right multiplication by nonnegative elements is monotone, the type $\text{WithBot } \alpha$ (which adds a bottom element $\bot$ to $\alpha$) also satisfies the property that right multiplication by nonnegative elements is monotone.
WithBot.instPosMulStrictMono instance
[MulZeroClass α] [Preorder α] [PosMulStrictMono α] : PosMulStrictMono (WithBot α)
Full source 
instance [MulZeroClass α] [Preorder α] [PosMulStrictMono α] : PosMulStrictMono (WithBot α) where
  elim := by
    intro ⟨x, x0⟩ a b h
    simp only [Subtype.coe_mk]
    lift x to α using x0.ne_bot
    induction b
    · exact absurd h not_lt_bot
    induction a
    · simp_rw [mul_bot x0.ne.symm, ← coe_mul, bot_lt_coe]
    simp only [← coe_mul, coe_lt_coe] at *
    norm_cast at x0
    exact mul_lt_mul_of_pos_left h x0
Strict Monotonicity of Left Multiplication by Positive Elements in $\text{WithBot } \alpha$
Informal description
For any type $\alpha$ with a multiplication operation, a zero element, and a preorder such that left multiplication by positive elements is strictly monotone, the type $\text{WithBot } \alpha$ (which extends $\alpha$ with a bottom element $\bot$) also satisfies the property that left multiplication by positive elements is strictly monotone.
WithBot.instMulPosStrictMono instance
[MulZeroClass α] [Preorder α] [MulPosStrictMono α] : MulPosStrictMono (WithBot α)
Full source 
instance [MulZeroClass α] [Preorder α] [MulPosStrictMono α] : MulPosStrictMono (WithBot α) where
  elim := by
    intro ⟨x, x0⟩ a b h
    simp only [Subtype.coe_mk]
    lift x to α using x0.ne_bot
    induction b
    · exact absurd h not_lt_bot
    induction a
    · simp_rw [bot_mul x0.ne.symm, ← coe_mul, bot_lt_coe]
    simp only [← coe_mul, coe_lt_coe] at *
    norm_cast at x0
    exact mul_lt_mul_of_pos_right h x0
Strict Monotonicity of Right Multiplication by Positive Elements in $\text{WithBot } \alpha$
Informal description
For any type $\alpha$ with a multiplication operation, a zero element, and a preorder such that right multiplication by positive elements is strictly monotone, the type $\text{WithBot } \alpha$ (which extends $\alpha$ with a bottom element $\bot$) also satisfies the property that right multiplication by positive elements is strictly monotone.
WithBot.instPosMulReflectLT instance
[MulZeroClass α] [Preorder α] [PosMulReflectLT α] : PosMulReflectLT (WithBot α)
Full source 
instance [MulZeroClass α] [Preorder α] [PosMulReflectLT α] : PosMulReflectLT (WithBot α) where
  elim := by
    intro ⟨x, x0⟩ a b h
    simp only [Subtype.coe_mk] at h
    rcases eq_or_ne x 0 with rfl | x0'
    · simp at h
    lift x to α
    · rintro rfl
      exact (WithBot.bot_lt_coe (0 : α)).not_le x0
    induction b
    · rw [mul_bot x0'] at h
      exact absurd h bot_le.not_lt
    induction a
    · exact WithBot.bot_lt_coe _
    simp only [← coe_mul, coe_lt_coe] at *
    norm_cast at x0
    exact lt_of_mul_lt_mul_left h x0
Strict Order Reflection by Left Multiplication in `WithBot α`
Informal description
For any type $\alpha$ with a multiplication operation, a zero element, and a preorder, if left multiplication by nonnegative elements reflects the strict order (i.e., `PosMulReflectLT α` holds), then the same property holds for the type `WithBot α` (which extends $\alpha$ with a bottom element $\bot$).
WithBot.instMulPosReflectLT instance
[MulZeroClass α] [Preorder α] [MulPosReflectLT α] : MulPosReflectLT (WithBot α)
Full source 
instance [MulZeroClass α] [Preorder α] [MulPosReflectLT α] : MulPosReflectLT (WithBot α) where
  elim := by
    intro ⟨x, x0⟩ a b h
    simp only [Subtype.coe_mk] at h
    rcases eq_or_ne x 0 with rfl | x0'
    · simp at h
    lift x to α
    · rintro rfl
      exact (WithBot.bot_lt_coe (0 : α)).not_le x0
    induction b
    · rw [bot_mul x0'] at h
      exact absurd h bot_le.not_lt
    induction a
    · exact WithBot.bot_lt_coe _
    simp only [← coe_mul, coe_lt_coe] at *
    norm_cast at x0
    exact lt_of_mul_lt_mul_right h x0
Strict Order Reflection by Right Multiplication in `WithBot α`
Informal description
For any type $\alpha$ with a multiplication operation, a zero element, and a preorder, if right multiplication by nonnegative elements reflects the strict order (i.e., `MulPosReflectLT α` holds), then the same property holds for the type `WithBot α` (which extends $\alpha$ with a bottom element $\bot$).
WithBot.instPosMulReflectLE instance
[MulZeroClass α] [Preorder α] [PosMulReflectLE α] : PosMulReflectLE (WithBot α)
Full source 
instance [MulZeroClass α] [Preorder α] [PosMulReflectLE α] : PosMulReflectLE (WithBot α) where
  elim := by
    intro ⟨x, x0⟩ a b h
    simp only [Subtype.coe_mk] at h
    lift x to α using x0.ne_bot
    induction a
    · exact bot_le
    induction b
    · rw [mul_bot x0.ne.symm, ← coe_mul] at h
      exact absurd h (bot_lt_coe _).not_le
    simp only [← coe_mul, coe_le_coe] at *
    norm_cast at x0
    exact le_of_mul_le_mul_left h x0
Non-strict Order Reflection by Left Multiplication in `WithBot α`
Informal description
For any type $\alpha$ with a multiplication operation, a zero element, and a preorder, if left multiplication by nonnegative elements reflects the non-strict order (i.e., `PosMulReflectLE α` holds), then the same property holds for the type `WithBot α` (which extends $\alpha$ with a bottom element $\bot$).
WithBot.instMulPosReflectLE instance
[MulZeroClass α] [Preorder α] [MulPosReflectLE α] : MulPosReflectLE (WithBot α)
Full source 
instance [MulZeroClass α] [Preorder α] [MulPosReflectLE α] : MulPosReflectLE (WithBot α) where
  elim := by
    intro ⟨x, x0⟩ a b h
    simp only [Subtype.coe_mk] at h
    lift x to α using x0.ne_bot
    induction a
    · exact bot_le
    induction b
    · rw [bot_mul x0.ne.symm, ← coe_mul] at h
      exact absurd h (bot_lt_coe _).not_le
    simp only [← coe_mul, coe_le_coe] at *
    norm_cast at x0
    exact le_of_mul_le_mul_right h x0
Non-strict Order Reflection under Right Multiplication in `WithBot α`
Informal description
For any type $\alpha$ with a multiplication operation, a zero element, and a preorder, if right multiplication by positive elements reflects the non-strict order (i.e., $\alpha$ satisfies `MulPosReflectLE`), then the same property holds for the type `WithBot α` (which extends $\alpha$ with a bottom element $\bot$).
WithBot.instIsOrderedRing instance
[CommSemiring α] [PartialOrder α] [IsOrderedRing α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] : IsOrderedRing (WithBot α)
Full source 
instance instIsOrderedRing [CommSemiring α] [PartialOrder α] [IsOrderedRing α]
    [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] :
    IsOrderedRing (WithBot α) where
  mul_le_mul_of_nonneg_left  _ _ _ := mul_le_mul_of_nonneg_left
  mul_le_mul_of_nonneg_right _ _ _ := mul_le_mul_of_nonneg_right
Ordered Ring Structure on $\text{WithBot }\alpha$
Informal description
For any commutative semiring $\alpha$ with a partial order, ordered ring structure, canonically ordered additive monoid structure, no zero divisors, and nontrivial structure, the type $\text{WithBot }\alpha$ (which adds a bottom element $\bot$ to $\alpha$) inherits an ordered ring structure. This means that the ring operations and order are extended to $\text{WithBot }\alpha$ in a way that preserves the ordered ring properties, including compatibility of the order with addition and multiplication by nonnegative elements.