Documentation

Mathlib.Algebra.Order.Ring.WithTop

Structures involving * and 0 on WithTop and WithBot#

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

instance WithTop.instDecidableEqWithTop {α : Type u_1} [inst : ] :
Equations
• WithTop.instDecidableEqWithTop = instDecidableEqOption
instance WithTop.instMulZeroClassWithTop {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] :
Equations
• One or more equations did not get rendered due to their size.
theorem WithTop.mul_def {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] {a : } {b : } :
a * b = if a = 0 b = 0 then 0 else Option.map₂ (fun x x_1 => x * x_1) a b
theorem WithTop.top_mul_top {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] :
theorem WithTop.mul_top' {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] (a : ) :
a * = if a = 0 then 0 else
@[simp]
theorem WithTop.mul_top {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] {a : } (h : a 0) :
theorem WithTop.top_mul' {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] (a : ) :
* a = if a = 0 then 0 else
@[simp]
theorem WithTop.top_mul {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] {a : } (h : a 0) :
theorem WithTop.mul_eq_top_iff {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] {a : } {b : } :
a * b = a 0 b = a = b 0
theorem WithTop.mul_lt_top' {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] [inst : LT α] {a : } {b : } (ha : a < ) (hb : b < ) :
a * b <
theorem WithTop.mul_lt_top {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] [inst : LT α] {a : } {b : } (ha : a ) (hb : b ) :
a * b <
instance WithTop.noZeroDivisors {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] [inst : ] :
Equations
@[simp]
theorem WithTop.coe_mul {α : Type u_1} [inst : ] [inst : ] {a : α} {b : α} :
↑(a * b) = a * b
theorem WithTop.mul_coe {α : Type u_1} [inst : ] [inst : ] {b : α} (hb : b 0) {a : } :
a * b = Option.bind a fun a => some (a * b)
@[simp]
theorem WithTop.untop'_zero_mul {α : Type u_1} [inst : ] [inst : ] (a : ) (b : ) :
WithTop.untop' 0 (a * b) = *
instance WithTop.instMulZeroOneClassWithTop {α : Type u_1} [inst : ] [inst : ] [inst : ] :

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

Equations
• WithTop.instMulZeroOneClassWithTop = let src := WithTop.instMulZeroClassWithTop; MulZeroOneClass.mk (_ : ∀ (a : ), 0 * a = 0) (_ : ∀ (a : ), a * 0 = 0)
@[simp]
theorem MonoidWithZeroHom.withTopMap_apply {R : Type u_1} {S : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] (f : R →*₀ S) (hf : ) :
↑() =
def MonoidWithZeroHom.withTopMap {R : Type u_1} {S : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] (f : R →*₀ S) (hf : ) :

A version of WithTop.map for MonoidWithZeroHoms.

Equations
• One or more equations did not get rendered due to their size.
instance WithTop.instSemigroupWithZeroWithTop {α : Type u_1} [inst : ] [inst : ] [inst : ] :
Equations
• WithTop.instSemigroupWithZeroWithTop = let src := WithTop.instMulZeroClassWithTop; SemigroupWithZero.mk (_ : ∀ (a : ), 0 * a = 0) (_ : ∀ (a : ), a * 0 = 0)
instance WithTop.monoidWithZero {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
instance WithTop.commMonoidWithZero {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] :
Equations
• WithTop.commMonoidWithZero = let src := WithTop.monoidWithZero; CommMonoidWithZero.mk (_ : ∀ (a : ), 0 * a = 0) (_ : ∀ (a : ), a * 0 = 0)
instance WithTop.commSemiring {α : Type u_1} [inst : ] [inst : ] [inst : ] :

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

Equations
• WithTop.commSemiring = let src := WithTop.addCommMonoidWithOne; let src_1 := WithTop.commMonoidWithZero; CommSemiring.mk (_ : ∀ (a b : ), a * b = b * a)
instance WithTop.instCanonicallyOrderedCommSemiringWithTop {α : Type u_1} [inst : ] [inst : ] [inst : ] :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem RingHom.withTopMap_apply {R : Type u_1} {S : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] (f : R →+* S) (hf : ) :
↑() = ().toFun
def RingHom.withTopMap {R : Type u_1} {S : Type u_2} [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] (f : R →+* S) (hf : ) :

A version of WithTop.map for RingHoms.

Equations
• One or more equations did not get rendered due to their size.
instance WithBot.instDecidableEqWithBot {α : Type u_1} [inst : ] :
Equations
• WithBot.instDecidableEqWithBot = instDecidableEqOption
instance WithBot.instMulZeroClassWithBot {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] :
Equations
• WithBot.instMulZeroClassWithBot = WithTop.instMulZeroClassWithTop
theorem WithBot.mul_def {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] {a : } {b : } :
a * b = if a = 0 b = 0 then 0 else Option.map₂ (fun x x_1 => x * x_1) a b
@[simp]
theorem WithBot.mul_bot {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] {a : } (h : a 0) :
@[simp]
theorem WithBot.bot_mul {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] {a : } (h : a 0) :
@[simp]
theorem WithBot.bot_mul_bot {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] :
theorem WithBot.mul_eq_bot_iff {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] {a : } {b : } :
a * b = a 0 b = a = b 0
theorem WithBot.bot_lt_mul' {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] [inst : LT α] {a : } {b : } (ha : < a) (hb : < b) :
< a * b
theorem WithBot.bot_lt_mul {α : Type u_1} [inst : ] [inst : Zero α] [inst : Mul α] [inst : LT α] {a : } {b : } (ha : a ) (hb : b ) :
< a * b
@[simp]
theorem WithBot.coe_mul {α : Type u_1} [inst : ] [inst : ] {a : α} {b : α} :
↑(a * b) = a * b
theorem WithBot.mul_coe {α : Type u_1} [inst : ] [inst : ] {b : α} (hb : b 0) {a : } :
a * b = Option.bind a fun a => some (a * b)
instance WithBot.instMulZeroOneClassWithBot {α : Type u_1} [inst : ] [inst : ] [inst : ] :

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

Equations
• WithBot.instMulZeroOneClassWithBot = WithTop.instMulZeroOneClassWithTop
instance WithBot.instNoZeroDivisorsWithBotToMulInstMulZeroClassWithBotToZeroZero {α : Type u_1} [inst : ] [inst : ] [inst : ] :
Equations
instance WithBot.instSemigroupWithZeroWithBot {α : Type u_1} [inst : ] [inst : ] [inst : ] :
Equations
• WithBot.instSemigroupWithZeroWithBot = WithTop.instSemigroupWithZeroWithTop
instance WithBot.instMonoidWithZeroWithBot {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] :
Equations
• WithBot.instMonoidWithZeroWithBot = WithTop.monoidWithZero
instance WithBot.commMonoidWithZero {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] :
Equations
• WithBot.commMonoidWithZero = WithTop.commMonoidWithZero
instance WithBot.commSemiring {α : Type u_1} [inst : ] [inst : ] [inst : ] :
Equations
• WithBot.commSemiring = WithTop.commSemiring
instance WithBot.instPosMulMonoWithBotToMulInstMulZeroClassWithBotToZeroZeroPreorder {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] :
Equations
instance WithBot.instMulPosMonoWithBotToMulInstMulZeroClassWithBotToZeroZeroPreorder {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] :
Equations
instance WithBot.instPosMulStrictMonoWithBotToMulInstMulZeroClassWithBotToZeroZeroPreorder {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] :
Equations
instance WithBot.instMulPosStrictMonoWithBotToMulInstMulZeroClassWithBotToZeroZeroPreorder {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] :
Equations
instance WithBot.instPosMulReflectLTWithBotToMulInstMulZeroClassWithBotToZeroZeroPreorder {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] :
Equations
instance WithBot.instMulPosReflectLTWithBotToMulInstMulZeroClassWithBotToZeroZeroPreorder {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] :
Equations
instance WithBot.instPosMulMonoRevWithBotToMulInstMulZeroClassWithBotToZeroZeroPreorder {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] :
Equations
instance WithBot.instMulPosMonoRevWithBotToMulInstMulZeroClassWithBotToZeroZeroPreorder {α : Type u_1} [inst : ] [inst : ] [inst : ] [inst : ] :
Equations
instance WithBot.orderedCommSemiring {α : Type u_1} [inst : ] [inst : ] [inst : ] :
Equations
• One or more equations did not get rendered due to their size.