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.

source
instance WithTop.instMulZeroClass {α : Type u_1} [DecidableEq α] [MulZeroClass α] :
MulZeroClass (WithTop α)
Equations
source
@[simp]
theorem WithTop.coe_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : α) (b : α) :
↑(a * b) = ↑a * ↑b
source
theorem WithTop.mul_top' {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : WithTop α) :
a * ⊤ = if a = 0 then 0 else ⊤
source
@[simp]
theorem WithTop.mul_top {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : WithTop α} (h : a ≠ 0) :
a * ⊤ = ⊤
source
theorem WithTop.top_mul' {α : Type u_1} [DecidableEq α] [MulZeroClass α] (b : WithTop α) :
⊤ * b = if b = 0 then 0 else ⊤
source
@[simp]
theorem WithTop.top_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] {b : WithTop α} (hb : b ≠ 0) :
⊤ * b = ⊤
source
@[simp]
theorem WithTop.top_mul_top {α : Type u_1} [DecidableEq α] [MulZeroClass α] :
⊤ * ⊤ = ⊤
source
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 (x x_1 : α) => x * x_1) a b
source
theorem WithTop.mul_eq_top_iff {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : WithTop α} {b : WithTop α} :
a * b = ⊤ ↔ a ≠ 0 ∧ b = ⊤ ∨ a = ⊤ ∧ b ≠ 0
source
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)
source
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)
source
@[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
source
theorem WithTop.mul_lt_top' {α : Type u_1} [DecidableEq α] [MulZeroClass α] [LT α] {a : WithTop α} {b : WithTop α} (ha : a < ⊤) (hb : b < ⊤) :
a * b < ⊤
source
theorem WithTop.mul_lt_top {α : Type u_1} [DecidableEq α] [MulZeroClass α] [LT α] {a : WithTop α} {b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
a * b < ⊤
source
instance WithTop.instNoZeroDivisors {α : Type u_1} [DecidableEq α] [MulZeroClass α] [NoZeroDivisors α] :
NoZeroDivisors (WithTop α)
Equations
  • ⋯ = ⋯
source
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 = let __spread.0 := WithTop.instMulZeroClass; MulZeroOneClass.mk ⋯ ⋯
source
@[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
source
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 = let __src := (↑f).withTopMap; let __src := (↑↑f).withTopMap; { toFun := WithTop.map ⇑f, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
Instances For
    source
    instance WithTop.instSemigroupWithZero {α : Type u_1} [DecidableEq α] [SemigroupWithZero α] [NoZeroDivisors α] :
    SemigroupWithZero (WithTop α)
    Equations
    source
    instance WithTop.instMonoidWithZero {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] :
    MonoidWithZero (WithTop α)
    Equations
    • WithTop.instMonoidWithZero = let __spread.0 := WithTop.instMulZeroOneClass; let __spread.1 := WithTop.instSemigroupWithZero; MonoidWithZero.mk ⋯ ⋯
    source
    @[simp]
    theorem WithTop.coe_pow {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] (a : α) (n : ℕ) :
    ↑(a ^ n) = ↑a ^ n
    source
    theorem WithTop.top_pow {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] {n : ℕ} (n_pos : 0 < n) :
    ⊤ ^ n = ⊤
    source
    instance WithTop.instCommMonoidWithZero {α : Type u_1} [DecidableEq α] [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] :
    CommMonoidWithZero (WithTop α)
    Equations
    source
    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 = let __src := WithTop.addCommMonoidWithOne; let __src_1 := WithTop.instCommMonoidWithZero; CommSemiring.mk ⋯
    source
    instance WithTop.instCanonicallyOrderedCommSemiringOfNontrivial {α : Type u_1} [DecidableEq α] [CanonicallyOrderedCommSemiring α] [Nontrivial α] :
    CanonicallyOrderedCommSemiring (WithTop α)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[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
    source
    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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance WithBot.instMulZeroClass {α : Type u_1} [DecidableEq α] [MulZeroClass α] :
      MulZeroClass (WithBot α)
      Equations
      • WithBot.instMulZeroClass = WithTop.instMulZeroClass
      source
      @[simp]
      theorem WithBot.coe_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : α) (b : α) :
      ↑(a * b) = ↑a * ↑b
      source
      theorem WithBot.mul_bot' {α : Type u_1} [DecidableEq α] [MulZeroClass α] (a : WithBot α) :
      a * ⊥ = if a = 0 then 0 else ⊥
      source
      @[simp]
      theorem WithBot.mul_bot {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : WithBot α} (h : a ≠ 0) :
      a * ⊥ = ⊥
      source
      theorem WithBot.bot_mul' {α : Type u_1} [DecidableEq α] [MulZeroClass α] (b : WithBot α) :
      ⊥ * b = if b = 0 then 0 else ⊥
      source
      @[simp]
      theorem WithBot.bot_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] {b : WithBot α} (hb : b ≠ 0) :
      ⊥ * b = ⊥
      source
      @[simp]
      theorem WithBot.bot_mul_bot {α : Type u_1} [DecidableEq α] [MulZeroClass α] :
      ⊥ * ⊥ = ⊥
      source
      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 (x x_1 : α) => x * x_1) a b
      source
      theorem WithBot.mul_eq_bot_iff {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a : WithBot α} {b : WithBot α} :
      a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0
      source
      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)
      source
      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)
      source
      @[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
      source
      theorem WithBot.bot_lt_mul' {α : Type u_1} [DecidableEq α] [MulZeroClass α] [LT α] {a : WithBot α} {b : WithBot α} (ha : ⊥ < a) (hb : ⊥ < b) :
      ⊥ < a * b
      source
      theorem WithBot.bot_lt_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] [LT α] {a : WithBot α} {b : WithBot α} (ha : a ≠ ⊥) (hb : b ≠ ⊥) :
      ⊥ < a * b
      source
      instance WithBot.instNoZeroDivisors {α : Type u_1} [DecidableEq α] [MulZeroClass α] [NoZeroDivisors α] :
      NoZeroDivisors (WithBot α)
      Equations
      • ⋯ = ⋯
      source
      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
      source
      instance WithBot.instSemigroupWithZero {α : Type u_1} [DecidableEq α] [SemigroupWithZero α] [NoZeroDivisors α] :
      SemigroupWithZero (WithBot α)
      Equations
      • WithBot.instSemigroupWithZero = WithTop.instSemigroupWithZero
      source
      instance WithBot.instMonoidWithZero {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] :
      MonoidWithZero (WithBot α)
      Equations
      • WithBot.instMonoidWithZero = WithTop.instMonoidWithZero
      source
      @[simp]
      theorem WithBot.coe_pow {α : Type u_1} [DecidableEq α] [MonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] (a : α) (n : ℕ) :
      ↑(a ^ n) = ↑a ^ n
      source
      instance WithBot.commMonoidWithZero {α : Type u_1} [DecidableEq α] [CommMonoidWithZero α] [NoZeroDivisors α] [Nontrivial α] :
      CommMonoidWithZero (WithBot α)
      Equations
      • WithBot.commMonoidWithZero = WithTop.instCommMonoidWithZero
      source
      instance WithBot.commSemiring {α : Type u_1} [DecidableEq α] [CanonicallyOrderedCommSemiring α] [Nontrivial α] :
      CommSemiring (WithBot α)
      Equations
      • WithBot.commSemiring = WithTop.commSemiring
      source
      instance WithBot.instPosMulMono {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [PosMulMono α] :
      PosMulMono (WithBot α)
      Equations
      • ⋯ = ⋯
      source
      instance WithBot.instMulPosMono {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [MulPosMono α] :
      MulPosMono (WithBot α)
      Equations
      • ⋯ = ⋯
      source
      instance WithBot.instPosMulStrictMono {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [PosMulStrictMono α] :
      PosMulStrictMono (WithBot α)
      Equations
      • ⋯ = ⋯
      source
      instance WithBot.instMulPosStrictMono {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [MulPosStrictMono α] :
      MulPosStrictMono (WithBot α)
      Equations
      • ⋯ = ⋯
      source
      instance WithBot.instPosMulReflectLT {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [PosMulReflectLT α] :
      PosMulReflectLT (WithBot α)
      Equations
      • ⋯ = ⋯
      source
      instance WithBot.instMulPosReflectLT {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [MulPosReflectLT α] :
      MulPosReflectLT (WithBot α)
      Equations
      • ⋯ = ⋯
      source
      instance WithBot.instPosMulReflectLE {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [PosMulReflectLE α] :
      PosMulReflectLE (WithBot α)
      Equations
      • ⋯ = ⋯
      source
      instance WithBot.instMulPosReflectLE {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [MulPosReflectLE α] :
      MulPosReflectLE (WithBot α)
      Equations
      • ⋯ = ⋯
      source
      instance WithBot.orderedCommSemiring {α : Type u_1} [DecidableEq α] [CanonicallyOrderedCommSemiring α] [Nontrivial α] :
      OrderedCommSemiring (WithBot α)
      Equations
      • WithBot.orderedCommSemiring = let __src := ⋯; let __src := WithBot.orderedAddCommMonoid; let __src_1 := WithBot.commSemiring; OrderedCommSemiring.mk ⋯