# Structures involving * and 0 on WithTop and WithBot#

The main results of this section are WithTop.canonicallyOrderedCommSemiring and WithBot.orderedCommSemiring.

instance WithTop.instMulZeroClass {α : Type u_1} [] [] :
Equations
• WithTop.instMulZeroClass =
@[simp]
theorem WithTop.coe_mul {α : Type u_1} [] [] (a : α) (b : α) :
(a * b) = a * b
theorem WithTop.mul_top' {α : Type u_1} [] [] (a : ) :
a * = if a = 0 then 0 else
@[simp]
theorem WithTop.mul_top {α : Type u_1} [] [] {a : } (h : a 0) :
theorem WithTop.top_mul' {α : Type u_1} [] [] (b : ) :
* b = if b = 0 then 0 else
@[simp]
theorem WithTop.top_mul {α : Type u_1} [] [] {b : } (hb : b 0) :
@[simp]
theorem WithTop.top_mul_top {α : Type u_1} [] [] :
theorem WithTop.mul_def {α : Type u_1} [] [] (a : ) (b : ) :
a * b = if a = 0 b = 0 then 0 else WithTop.map₂ (fun (x x_1 : α) => x * x_1) a b
theorem WithTop.mul_eq_top_iff {α : Type u_1} [] [] {a : } {b : } :
a * b = a 0 b = a = b 0
theorem WithTop.mul_coe_eq_bind {α : Type u_1} [] [] {b : α} (hb : b 0) (a : ) :
a * b = Option.bind a fun (a : α) => some (a * b)
theorem WithTop.coe_mul_eq_bind {α : Type u_1} [] [] {a : α} (ha : a 0) (b : ) :
a * b = Option.bind b fun (b : α) => some (a * b)
@[simp]
theorem WithTop.untop'_zero_mul {α : Type u_1} [] [] (a : ) (b : ) :
WithTop.untop' 0 (a * b) = *
theorem WithTop.mul_lt_top' {α : Type u_1} [] [] [LT α] {a : } {b : } (ha : a < ) (hb : b < ) :
a * b <
theorem WithTop.mul_lt_top {α : Type u_1} [] [] [LT α] {a : } {b : } (ha : a ) (hb : b ) :
a * b <
instance WithTop.instNoZeroDivisors {α : Type u_1} [] [] [] :
Equations
• =
instance WithTop.instMulZeroOneClass {α : Type u_1} [] [] [] :

Nontrivial α is needed here as otherwise we have 1 * ⊤ = ⊤ but also 0 * ⊤ = 0.

Equations
• WithTop.instMulZeroOneClass = let __spread.0 := WithTop.instMulZeroClass;
@[simp]
theorem MonoidWithZeroHom.withTopMap_apply {R : Type u_2} {S : Type u_3} [] [] [] [] [] [] (f : R →*₀ S) (hf : ) :
(f.withTopMap hf) =
def MonoidWithZeroHom.withTopMap {R : Type u_2} {S : Type u_3} [] [] [] [] [] [] (f : R →*₀ S) (hf : ) :

A version of WithTop.map for MonoidWithZeroHoms.

Equations
• f.withTopMap hf = let __src := f.withTopMap; let __src := (f).withTopMap; { toFun := , map_zero' := , map_one' := , map_mul' := }
Instances For
instance WithTop.instSemigroupWithZero {α : Type u_1} [] [] :
Equations
• WithTop.instSemigroupWithZero = let __spread.0 := WithTop.instMulZeroClass;
instance WithTop.instMonoidWithZero {α : Type u_1} [] [] [] [] :
Equations
@[simp]
theorem WithTop.coe_pow {α : Type u_1} [] [] [] [] (a : α) (n : ) :
(a ^ n) = a ^ n
instance WithTop.instCommMonoidWithZero {α : Type u_1} [] [] [] :
Equations
• WithTop.instCommMonoidWithZero = let __spread.0 := WithTop.instMonoidWithZero;
instance WithTop.commSemiring {α : Type u_1} [] [] :

This instance requires CanonicallyOrderedCommSemiring as it is the smallest class that derives from both NonAssocNonUnitalSemiring and CanonicallyOrderedAddCommMonoid, both of which are required for distributivity.

Equations
• WithTop.commSemiring = let __src := WithTop.addCommMonoidWithOne; let __src_1 := WithTop.instCommMonoidWithZero;
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem RingHom.withTopMap_apply {R : Type u_2} {S : Type u_3} [] [] [] [] (f : R →+* S) (hf : ) :
(f.withTopMap hf) = (f.toMonoidWithZeroHom.withTopMap hf).toFun
def RingHom.withTopMap {R : Type u_2} {S : Type u_3} [] [] [] [] (f : R →+* S) (hf : ) :

A version of WithTop.map for RingHoms.

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance WithBot.instMulZeroClass {α : Type u_1} [] [] :
Equations
• WithBot.instMulZeroClass = WithTop.instMulZeroClass
@[simp]
theorem WithBot.coe_mul {α : Type u_1} [] [] (a : α) (b : α) :
(a * b) = a * b
theorem WithBot.mul_bot' {α : Type u_1} [] [] (a : ) :
a * = if a = 0 then 0 else
@[simp]
theorem WithBot.mul_bot {α : Type u_1} [] [] {a : } (h : a 0) :
theorem WithBot.bot_mul' {α : Type u_1} [] [] (b : ) :
* b = if b = 0 then 0 else
@[simp]
theorem WithBot.bot_mul {α : Type u_1} [] [] {b : } (hb : b 0) :
@[simp]
theorem WithBot.bot_mul_bot {α : Type u_1} [] [] :
theorem WithBot.mul_def {α : Type u_1} [] [] (a : ) (b : ) :
a * b = if a = 0 b = 0 then 0 else WithBot.map₂ (fun (x x_1 : α) => x * x_1) a b
theorem WithBot.mul_eq_bot_iff {α : Type u_1} [] [] {a : } {b : } :
a * b = a 0 b = a = b 0
theorem WithBot.mul_coe_eq_bind {α : Type u_1} [] [] {b : α} (hb : b 0) (a : ) :
a * b = Option.bind a fun (a : α) => some (a * b)
theorem WithBot.coe_mul_eq_bind {α : Type u_1} [] [] {a : α} (ha : a 0) (b : ) :
a * b = Option.bind b fun (b : α) => some (a * b)
@[simp]
theorem WithBot.unbot'_zero_mul {α : Type u_1} [] [] (a : ) (b : ) :
WithBot.unbot' 0 (a * b) = *
theorem WithBot.bot_lt_mul' {α : Type u_1} [] [] [LT α] {a : } {b : } (ha : < a) (hb : < b) :
< a * b
theorem WithBot.bot_lt_mul {α : Type u_1} [] [] [LT α] {a : } {b : } (ha : a ) (hb : b ) :
< a * b
instance WithBot.instNoZeroDivisors {α : Type u_1} [] [] [] :
Equations
• =
instance WithBot.instMulZeroOneClass {α : Type u_1} [] [] [] :

Nontrivial α is needed here as otherwise we have 1 * ⊥ = ⊥ but also = 0 * ⊥ = 0.

Equations
• WithBot.instMulZeroOneClass = WithTop.instMulZeroOneClass
instance WithBot.instSemigroupWithZero {α : Type u_1} [] [] :
Equations
• WithBot.instSemigroupWithZero = WithTop.instSemigroupWithZero
instance WithBot.instMonoidWithZero {α : Type u_1} [] [] [] [] :
Equations
• WithBot.instMonoidWithZero = WithTop.instMonoidWithZero
@[simp]
theorem WithBot.coe_pow {α : Type u_1} [] [] [] [] (a : α) (n : ) :
(a ^ n) = a ^ n
instance WithBot.commMonoidWithZero {α : Type u_1} [] [] [] :
Equations
• WithBot.commMonoidWithZero = WithTop.instCommMonoidWithZero
instance WithBot.commSemiring {α : Type u_1} [] [] :
Equations
• WithBot.commSemiring = WithTop.commSemiring
instance WithBot.instPosMulMono {α : Type u_1} [] [] [] [] :
Equations
• =
instance WithBot.instMulPosMono {α : Type u_1} [] [] [] [] :
Equations
• =
instance WithBot.instPosMulStrictMono {α : Type u_1} [] [] [] [] :
Equations
• =
instance WithBot.instMulPosStrictMono {α : Type u_1} [] [] [] [] :
Equations
• =
instance WithBot.instPosMulReflectLT {α : Type u_1} [] [] [] [] :
Equations
• =
instance WithBot.instMulPosReflectLT {α : Type u_1} [] [] [] [] :
Equations
• =
instance WithBot.instPosMulReflectLE {α : Type u_1} [] [] [] [] :
Equations
• =
instance WithBot.instMulPosReflectLE {α : Type u_1} [] [] [] [] :
Equations
• =
instance WithBot.orderedCommSemiring {α : Type u_1} [] [] :
Equations
• WithBot.orderedCommSemiring = let __src := ; let __src := WithBot.orderedAddCommMonoid; let __src_1 := WithBot.commSemiring;