Structures involving `*` and `0` on `WithTop` and `WithBot` #

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

source

ink

instance WithTop.instDecidableEqWithTop {α : Type u_1} [inst : DecidableEq α] :

DecidableEq (WithTop α)

Equations

WithTop.instDecidableEqWithTop = instDecidableEqOption

source

ink

instance WithTop.instMulZeroClassWithTop {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] :

MulZeroClass (WithTop α)

Equations

One or more equations did not get rendered due to their size.

source

ink

theorem WithTop.mul_def {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] {a : WithTop α} {b : WithTop α} :

a * b = if a = 0 ∨ b = 0 then 0 else Option.map₂ (fun x x_1 => x * x_1) a b

source

ink

theorem WithTop.top_mul_top {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] :

⊤ * ⊤ = ⊤

source

ink

theorem WithTop.mul_top' {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] (a : WithTop α) :

a * ⊤ = if a = 0 then 0 else ⊤

source

ink

@[simp]

theorem WithTop.mul_top {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] {a : WithTop α} (h : a ≠ 0) :

a * ⊤ = ⊤

source

ink

theorem WithTop.top_mul' {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] (a : WithTop α) :

⊤ * a = if a = 0 then 0 else ⊤

source

ink

@[simp]

theorem WithTop.top_mul {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] {a : WithTop α} (h : a ≠ 0) :

⊤ * a = ⊤

source

ink

theorem WithTop.mul_eq_top_iff {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] {a : WithTop α} {b : WithTop α} :

a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0

source

ink

theorem WithTop.mul_lt_top' {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] [inst : LT α] {a : WithTop α} {b : WithTop α} (ha : a < ⊤) (hb : b < ⊤) :

a * b < ⊤

source

ink

theorem WithTop.mul_lt_top {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] [inst : LT α] {a : WithTop α} {b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :

a * b < ⊤

source

ink

instance WithTop.noZeroDivisors {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] [inst : NoZeroDivisors α] :

NoZeroDivisors (WithTop α)

Equations

@WithTop.noZeroDivisors = @WithTop.noZeroDivisors.proof_1

source

ink

@[simp]

theorem WithTop.coe_mul {α : Type u_1} [inst : DecidableEq α] [inst : MulZeroClass α] {a : α} {b : α} :

↑(a * b) = ↑a * ↑b

source

ink

theorem WithTop.mul_coe {α : Type u_1} [inst : DecidableEq α] [inst : MulZeroClass α] {b : α} (hb : b ≠ 0) {a : WithTop α} :

a * ↑b = Option.bind a fun a => some (a * b)

source

ink

@[simp]

theorem WithTop.untop'_zero_mul {α : Type u_1} [inst : DecidableEq α] [inst : MulZeroClass α] (a : WithTop α) (b : WithTop α) :

WithTop.untop' 0 (a * b) = WithTop.untop' 0 a * WithTop.untop' 0 b

source

ink

instance WithTop.instMulZeroOneClassWithTop {α : Type u_1} [inst : DecidableEq α] [inst : MulZeroOneClass α] [inst : Nontrivial α] :

MulZeroOneClass (WithTop α)

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

Equations

WithTop.instMulZeroOneClassWithTop = let src := WithTop.instMulZeroClassWithTop; MulZeroOneClass.mk (_ : ∀ (a : WithTop α), 0 * a = 0) (_ : ∀ (a : WithTop α), a * 0 = 0)

source

ink

@[simp]

theorem MonoidWithZeroHom.withTopMap_apply {R : Type u_1} {S : Type u_2} [inst : MulZeroOneClass R] [inst : DecidableEq R] [inst : Nontrivial R] [inst : MulZeroOneClass S] [inst : DecidableEq S] [inst : Nontrivial S] (f : R →*₀ S) (hf : Function.Injective ↑f) :

↑(MonoidWithZeroHom.withTopMap f hf) = WithTop.map ↑f

source

ink

def MonoidWithZeroHom.withTopMap {R : Type u_1} {S : Type u_2} [inst : MulZeroOneClass R] [inst : DecidableEq R] [inst : Nontrivial R] [inst : MulZeroOneClass S] [inst : DecidableEq S] [inst : Nontrivial S] (f : R →*₀ S) (hf : Function.Injective ↑f) :

WithTop R →*₀ WithTop S

A version of WithTop.map for MonoidWithZeroHoms.

Equations

One or more equations did not get rendered due to their size.

source

ink

instance WithTop.instSemigroupWithZeroWithTop {α : Type u_1} [inst : DecidableEq α] [inst : SemigroupWithZero α] [inst : NoZeroDivisors α] :

SemigroupWithZero (WithTop α)

Equations

WithTop.instSemigroupWithZeroWithTop = let src := WithTop.instMulZeroClassWithTop; SemigroupWithZero.mk (_ : ∀ (a : WithTop α), 0 * a = 0) (_ : ∀ (a : WithTop α), a * 0 = 0)

source

ink

instance WithTop.monoidWithZero {α : Type u_1} [inst : DecidableEq α] [inst : MonoidWithZero α] [inst : NoZeroDivisors α] [inst : Nontrivial α] :

MonoidWithZero (WithTop α)

Equations

One or more equations did not get rendered due to their size.

source

ink

instance WithTop.commMonoidWithZero {α : Type u_1} [inst : DecidableEq α] [inst : CommMonoidWithZero α] [inst : NoZeroDivisors α] [inst : Nontrivial α] :

CommMonoidWithZero (WithTop α)

Equations

WithTop.commMonoidWithZero = let src := WithTop.monoidWithZero; CommMonoidWithZero.mk (_ : ∀ (a : WithTop α), 0 * a = 0) (_ : ∀ (a : WithTop α), a * 0 = 0)

source

ink

instance WithTop.commSemiring {α : Type u_1} [inst : DecidableEq α] [inst : CanonicallyOrderedCommSemiring α] [inst : Nontrivial α] :

CommSemiring (WithTop α)

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 : WithTop α), a * b = b * a)

source

ink

instance WithTop.instCanonicallyOrderedCommSemiringWithTop {α : Type u_1} [inst : DecidableEq α] [inst : CanonicallyOrderedCommSemiring α] [inst : Nontrivial α] :

CanonicallyOrderedCommSemiring (WithTop α)

Equations

One or more equations did not get rendered due to their size.

source

ink

@[simp]

theorem RingHom.withTopMap_apply {R : Type u_1} {S : Type u_2} [inst : CanonicallyOrderedCommSemiring R] [inst : DecidableEq R] [inst : Nontrivial R] [inst : CanonicallyOrderedCommSemiring S] [inst : DecidableEq S] [inst : Nontrivial S] (f : R →+* S) (hf : Function.Injective ↑f) :

↑(RingHom.withTopMap f hf) = (↑(MonoidWithZeroHom.withTopMap (RingHom.toMonoidWithZeroHom f) hf)).toFun

source

ink

def RingHom.withTopMap {R : Type u_1} {S : Type u_2} [inst : CanonicallyOrderedCommSemiring R] [inst : DecidableEq R] [inst : Nontrivial R] [inst : CanonicallyOrderedCommSemiring S] [inst : DecidableEq S] [inst : Nontrivial S] (f : R →+* S) (hf : Function.Injective ↑f) :

WithTop R →+* WithTop S

A version of WithTop.map for RingHoms.

Equations

One or more equations did not get rendered due to their size.

source

ink

instance WithBot.instDecidableEqWithBot {α : Type u_1} [inst : DecidableEq α] :

DecidableEq (WithBot α)

Equations

WithBot.instDecidableEqWithBot = instDecidableEqOption

source

ink

instance WithBot.instMulZeroClassWithBot {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] :

MulZeroClass (WithBot α)

Equations

WithBot.instMulZeroClassWithBot = WithTop.instMulZeroClassWithTop

source

ink

theorem WithBot.mul_def {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] {a : WithBot α} {b : WithBot α} :

a * b = if a = 0 ∨ b = 0 then 0 else Option.map₂ (fun x x_1 => x * x_1) a b

source

ink

@[simp]

theorem WithBot.mul_bot {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] {a : WithBot α} (h : a ≠ 0) :

a * ⊥ = ⊥

source

ink

@[simp]

theorem WithBot.bot_mul {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] {a : WithBot α} (h : a ≠ 0) :

⊥ * a = ⊥

source

ink

@[simp]

theorem WithBot.bot_mul_bot {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] :

⊥ * ⊥ = ⊥

source

ink

theorem WithBot.mul_eq_bot_iff {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] {a : WithBot α} {b : WithBot α} :

a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0

source

ink

theorem WithBot.bot_lt_mul' {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] [inst : LT α] {a : WithBot α} {b : WithBot α} (ha : ⊥ < a) (hb : ⊥ < b) :

⊥ < a * b

source

ink

theorem WithBot.bot_lt_mul {α : Type u_1} [inst : DecidableEq α] [inst : Zero α] [inst : Mul α] [inst : LT α] {a : WithBot α} {b : WithBot α} (ha : a ≠ ⊥) (hb : b ≠ ⊥) :

⊥ < a * b

source

ink

@[simp]