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} [DecidableEq α] [MulZeroClass α] : MulZeroClass (WithTop α)

Equations

• WithTop.instMulZeroClass = MulZeroClass.mk ⋯ ⋯

@[simp]

theorem WithTop.coe_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : α) (b : α) : ↑(a * b) = ↑a * ↑b

theorem WithTop.mul_top' {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : WithTop α) : a * ⊤ = if a = 0 then 0 else ⊤

@[simp]

theorem WithTop.mul_top {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : WithTop α} (h : a ≠ 0) : a * ⊤ = ⊤

theorem WithTop.top_mul' {α : Type u_1} [DecidableEq α] [MulZeroClass α] (b : WithTop α) : ⊤ * b = if b = 0 then 0 else ⊤

@[simp]

theorem WithTop.top_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] {b : WithTop α} (hb : b ≠ 0) : ⊤ * b = ⊤

@[simp]

theorem WithTop.top_mul_top {α : Type u_1} [DecidableEq α] [MulZeroClass α] : ⊤ * ⊤ = ⊤

theorem WithTop.mul_def {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : WithTop α) (b : WithTop α) : a * b = if a = 0 ∨ b = 0 then 0 else WithTop.map₂ (fun (x1 x2 : α) => x1 * x2) a b

theorem WithTop.mul_eq_top_iff {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : WithTop α} {b : WithTop α} : a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0

theorem WithTop.mul_coe_eq_bind {α : Type u_1} [DecidableEq α] [MulZeroClass α] {b : α} (hb : b ≠ 0) (a : WithTop α) : a * ↑b = Option.bind a fun (a : α) => some (a * b)

theorem WithTop.coe_mul_eq_bind {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : α} (ha : a ≠ 0) (b : WithTop α) : ↑a * b = Option.bind b fun (b : α) => some (a * b)

@[simp]

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

theorem WithTop.mul_ne_top {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : WithTop α} {b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) : a * b ≠ ⊤

theorem WithTop.mul_lt_top {α : Type u_1} [DecidableEq α] [MulZeroClass α] [LT α] {a : WithTop α} {b : WithTop α} (ha : a < ⊤) (hb : b < ⊤) : a * b < ⊤

@[deprecated WithTop.mul_lt_top]

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

Alias of WithTop.mul_lt_top.

instance WithTop.instNoZeroDivisors {α : Type u_1} [DecidableEq α] [MulZeroClass α] [NoZeroDivisors α] : NoZeroDivisors (WithTop α)

Equations

• ⋯ = ⋯

instance WithTop.instMulZeroOneClass {α : Type u_1} [DecidableEq α] [MulZeroOneClass α] [Nontrivial α] : MulZeroOneClass (WithTop α)

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

Equations

• WithTop.instMulZeroOneClass = MulZeroOneClass.mk ⋯ ⋯

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

A version of WithTop.map for MonoidWithZeroHoms.

Equations

• f.withTopMap hf = { toFun := WithTop.map ⇑f, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MonoidWithZeroHom.withTopMap_apply {R : Type u_2} {S : Type u_3} [MulZeroOneClass R] [DecidableEq R] [Nontrivial R] [MulZeroOneClass S] [DecidableEq S] [Nontrivial S] (f : R →*₀ S) (hf : Function.Injective ⇑f) : ⇑(f.withTopMap hf) = WithTop.map ⇑f

instance WithTop.instSemigroupWithZero {α : Type u_1} [DecidableEq α] [SemigroupWithZero α] [NoZeroDivisors α] : SemigroupWithZero (WithTop α)

Equations

• WithTop.instSemigroupWithZero = SemigroupWithZero.mk ⋯ ⋯

instance WithTop.instMonoidWithZero {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] : MonoidWithZero (WithTop α)

Equations

• WithTop.instMonoidWithZero = MonoidWithZero.mk ⋯ ⋯

@[simp]

theorem WithTop.coe_pow {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] (a : α) (n : ℕ) : ↑(a ^ n) = ↑a ^ n

theorem WithTop.top_pow {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {n : ℕ} (n_pos : 0 < n) : ⊤ ^ n = ⊤

instance WithTop.instCommMonoidWithZero {α : Type u_1} [DecidableEq α] [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] : CommMonoidWithZero (WithTop α)

Equations

• WithTop.instCommMonoidWithZero = CommMonoidWithZero.mk ⋯ ⋯

instance WithTop.commSemiring {α : Type u_1} [DecidableEq α] [CanonicallyOrderedCommSemiring α] [Nontrivial α] : CommSemiring (WithTop α)

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 = CommSemiring.mk ⋯

instance WithTop.instCanonicallyOrderedCommSemiringOfNontrivial {α : Type u_1} [DecidableEq α] [CanonicallyOrderedCommSemiring α] [Nontrivial α] : CanonicallyOrderedCommSemiring (WithTop α)

Equations

• WithTop.instCanonicallyOrderedCommSemiringOfNontrivial = CanonicallyOrderedCommSemiring.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ Semiring.npow ⋯ ⋯ ⋯ ⋯

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

A version of WithTop.map for RingHoms.

Equations

• f.withTopMap hf = { toFun := (↑(f.toMonoidWithZeroHom.withTopMap hf)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem RingHom.withTopMap_apply {R : Type u_2} {S : Type u_3} [CanonicallyOrderedCommSemiring R] [DecidableEq R] [Nontrivial R] [CanonicallyOrderedCommSemiring S] [DecidableEq S] [Nontrivial S] (f : R →+* S) (hf : Function.Injective ⇑f) : ⇑(f.withTopMap hf) = (↑(f.toMonoidWithZeroHom.withTopMap hf)).toFun

theorem WithTop.mul_lt_mul {α : Type u_1} [DecidableEq α] [CanonicallyOrderedCommSemiring α] [PosMulStrictMono α] {a₁ : WithTop α} {a₂ : WithTop α} {b₁ : WithTop α} {b₂ : WithTop α} (ha : a₁ < a₂) (hb : b₁ < b₂) : a₁ * b₁ < a₂ * b₂

theorem WithTop.pow_right_strictMono {α : Type u_1} [DecidableEq α] [CanonicallyOrderedCommSemiring α] [PosMulStrictMono α] [NoZeroDivisors α] [Nontrivial α] {n : ℕ} : n ≠ 0 → StrictMono fun (a : WithTop α) => a ^ n

theorem WithTop.pow_lt_pow_left {α : Type u_1} [DecidableEq α] [CanonicallyOrderedCommSemiring α] [PosMulStrictMono α] [NoZeroDivisors α] [Nontrivial α] {a : WithTop α} {b : WithTop α} (hab : a < b) {n : ℕ} (hn : n ≠ 0) : a ^ n < b ^ n

instance WithBot.instMulZeroClass {α : Type u_1} [DecidableEq α] [MulZeroClass α] : MulZeroClass (WithBot α)

Equations

• WithBot.instMulZeroClass = WithTop.instMulZeroClass

@[simp]

theorem WithBot.coe_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : α) (b : α) : ↑(a * b) = ↑a * ↑b

theorem WithBot.mul_bot' {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : WithBot α) : a * ⊥ = if a = 0 then 0 else ⊥

@[simp]

theorem WithBot.mul_bot {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : WithBot α} (h : a ≠ 0) : a * ⊥ = ⊥

theorem WithBot.bot_mul' {α : Type u_1} [DecidableEq α] [MulZeroClass α] (b : WithBot α) : ⊥ * b = if b = 0 then 0 else ⊥

@[simp]

theorem WithBot.bot_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] {b : WithBot α} (hb : b ≠ 0) : ⊥ * b = ⊥

@[simp]

theorem WithBot.bot_mul_bot {α : Type u_1} [DecidableEq α] [MulZeroClass α] : ⊥ * ⊥ = ⊥

theorem WithBot.mul_def {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : WithBot α) (b : WithBot α) : a * b = if a = 0 ∨ b = 0 then 0 else WithBot.map₂ (fun (x1 x2 : α) => x1 * x2) a b

theorem WithBot.mul_eq_bot_iff {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : WithBot α} {b : WithBot α} : a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0

theorem WithBot.mul_coe_eq_bind {α : Type u_1} [DecidableEq α] [MulZeroClass α] {b : α} (hb : b ≠ 0) (a : WithBot α) : a * ↑b = Option.bind a fun (a : α) => some (a * b)

theorem WithBot.coe_mul_eq_bind {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : α} (ha : a ≠ 0) (b : WithBot α) : ↑a * b = Option.bind b fun (b : α) => some (a * b)

@[simp]

theorem WithBot.unbot'_zero_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : WithBot α) (b : WithBot α) : WithBot.unbot' 0 (a * b) = WithBot.unbot' 0 a * WithBot.unbot' 0 b

theorem WithBot.mul_ne_bot {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : WithBot α} {b : WithBot α} (ha : a ≠ ⊥) (hb : b ≠ ⊥) : a * b ≠ ⊥

theorem WithBot.bot_lt_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] [LT α] {a : WithBot α} {b : WithBot α} (ha : ⊥ < a) (hb : ⊥ < b) : ⊥ < a * b

@[deprecated WithBot.bot_lt_mul]

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

Alias of WithBot.bot_lt_mul.

instance WithBot.instNoZeroDivisors {α : Type u_1} [DecidableEq α] [MulZeroClass α] [NoZeroDivisors α] : NoZeroDivisors (WithBot α)

Equations

• ⋯ = ⋯

instance WithBot.instMulZeroOneClass {α : Type u_1} [DecidableEq α] [MulZeroOneClass α] [Nontrivial α] : MulZeroOneClass (WithBot α)

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

Equations

• WithBot.instMulZeroOneClass = WithTop.instMulZeroOneClass

instance WithBot.instSemigroupWithZero {α : Type u_1} [DecidableEq α] [SemigroupWithZero α] [NoZeroDivisors α] : SemigroupWithZero (WithBot α)

Equations

• WithBot.instSemigroupWithZero = WithTop.instSemigroupWithZero

instance WithBot.instMonoidWithZero {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] : MonoidWithZero (WithBot α)

Equations

• WithBot.instMonoidWithZero = WithTop.instMonoidWithZero

@[simp]

theorem WithBot.coe_pow {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] (a : α) (n : ℕ) : ↑(a ^ n) = ↑a ^ n

instance WithBot.commMonoidWithZero {α : Type u_1} [DecidableEq α] [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] : CommMonoidWithZero (WithBot α)

Equations

• WithBot.commMonoidWithZero = WithTop.instCommMonoidWithZero

instance WithBot.commSemiring {α : Type u_1} [DecidableEq α] [CanonicallyOrderedCommSemiring α] [Nontrivial α] : CommSemiring (WithBot α)

Equations

• WithBot.commSemiring = WithTop.commSemiring

instance WithBot.instPosMulMono {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [PosMulMono α] : PosMulMono (WithBot α)

Equations

• ⋯ = ⋯

instance WithBot.instMulPosMono {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [MulPosMono α] : MulPosMono (WithBot α)

Equations

• ⋯ = ⋯

instance WithBot.instPosMulStrictMono {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [PosMulStrictMono α] : PosMulStrictMono (WithBot α)

Equations

• ⋯ = ⋯

instance WithBot.instMulPosStrictMono {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [MulPosStrictMono α] : MulPosStrictMono (WithBot α)

Equations

• ⋯ = ⋯

instance WithBot.instPosMulReflectLT {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [PosMulReflectLT α] : PosMulReflectLT (WithBot α)

Equations

• ⋯ = ⋯

instance WithBot.instMulPosReflectLT {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [MulPosReflectLT α] : MulPosReflectLT (WithBot α)

Equations

• ⋯ = ⋯

instance WithBot.instPosMulReflectLE {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [PosMulReflectLE α] : PosMulReflectLE (WithBot α)

Equations

• ⋯ = ⋯

instance WithBot.instMulPosReflectLE {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [MulPosReflectLE α] : MulPosReflectLE (WithBot α)

Equations

• ⋯ = ⋯

instance WithBot.orderedCommSemiring {α : Type u_1} [DecidableEq α] [CanonicallyOrderedCommSemiring α] [Nontrivial α] : OrderedCommSemiring (WithBot α)

Equations

• WithBot.orderedCommSemiring = OrderedCommSemiring.mk ⋯