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 b : WithTop α) :
a * b = if a = 0 ∨ b = 0 then 0 else WithTop.map₂ (fun (x1 x2 : α) => x1 * x2) a b
source
theorem WithTop.mul_eq_top_iff {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a 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 b : WithTop α) :
WithTop.untop' 0 (a * b) = WithTop.untop' 0 a * WithTop.untop' 0 b
source
theorem WithTop.mul_ne_top {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤) :
a * b ≠ ⊤
source
theorem WithTop.mul_lt_top {α : Type u_1} [DecidableEq α] [MulZeroClass α] [LT α] {a b : WithTop α} (ha : a < ⊤) (hb : b < ⊤) :
a * b < ⊤
source
@[deprecated WithTop.mul_lt_top]
theorem WithTop.mul_lt_top' {α : Type u_1} [DecidableEq α] [MulZeroClass α] [LT α] {a b : WithTop α} (ha : a < ⊤) (hb : b < ⊤) :
a * b < ⊤

Alias of WithTop.mul_lt_top.

source
theorem WithTop.instNoZeroDivisors {α : Type u_1} [DecidableEq α] [MulZeroClass α] [NoZeroDivisors α] :
NoZeroDivisors (WithTop α)
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
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 = { toFun := WithTop.map ⇑f, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
Instances For
    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
    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
    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
    source
    instance WithTop.instCanonicallyOrderedCommSemiringOfNontrivial {α : Type u_1} [DecidableEq α] [CanonicallyOrderedCommSemiring α] [Nontrivial α] :
    CanonicallyOrderedCommSemiring (WithTop α)
    Equations
    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
    • f.withTopMap hf = { toFun := (↑(f.toMonoidWithZeroHom.withTopMap hf)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
    Instances For
      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
      theorem WithTop.mul_lt_mul {α : Type u_1} [DecidableEq α] [CanonicallyOrderedCommSemiring α] [PosMulStrictMono α] {a₁ a₂ b₁ b₂ : WithTop α} (ha : a₁ < a₂) (hb : b₁ < b₂) :
      a₁ * b₁ < a₂ * b₂
      source
      theorem WithTop.pow_right_strictMono {α : Type u_1} [DecidableEq α] [CanonicallyOrderedCommSemiring α] [PosMulStrictMono α] [NoZeroDivisors α] [Nontrivial α] {n : ℕ} :
      n ≠ 0 → StrictMono fun (a : WithTop α) => a ^ n
      source
      theorem WithTop.pow_lt_pow_left {α : Type u_1} [DecidableEq α] [CanonicallyOrderedCommSemiring α] [PosMulStrictMono α] [NoZeroDivisors α] [Nontrivial α] {a b : WithTop α} (hab : a < b) {n : ℕ} (hn : n ≠ 0) :
      a ^ n < b ^ n
      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 b : WithBot α) :
      a * b = if a = 0 ∨ b = 0 then 0 else WithBot.map₂ (fun (x1 x2 : α) => x1 * x2) a b
      source
      theorem WithBot.mul_eq_bot_iff {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a 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 b : WithBot α) :
      WithBot.unbot' 0 (a * b) = WithBot.unbot' 0 a * WithBot.unbot' 0 b
      source
      theorem WithBot.mul_ne_bot {α : Type u_1} [DecidableEq α] [MulZeroClass α] {a b : WithBot α} (ha : a ≠ ⊥) (hb : b ≠ ⊥) :
      a * b ≠ ⊥
      source
      theorem WithBot.bot_lt_mul {α : Type u_1} [DecidableEq α] [MulZeroClass α] [LT α] {a b : WithBot α} (ha : ⊥ < a) (hb : ⊥ < b) :
      ⊥ < a * b
      source
      @[deprecated WithBot.bot_lt_mul]
      theorem WithBot.bot_lt_mul' {α : Type u_1} [DecidableEq α] [MulZeroClass α] [LT α] {a b : WithBot α} (ha : ⊥ < a) (hb : ⊥ < b) :
      ⊥ < a * b

      Alias of WithBot.bot_lt_mul.

      source
      theorem WithBot.instNoZeroDivisors {α : Type u_1} [DecidableEq α] [MulZeroClass α] [NoZeroDivisors α] :
      NoZeroDivisors (WithBot α)
      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
      theorem WithBot.instPosMulMono {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [PosMulMono α] :
      PosMulMono (WithBot α)
      source
      theorem WithBot.instMulPosMono {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [MulPosMono α] :
      MulPosMono (WithBot α)
      source
      theorem WithBot.instPosMulStrictMono {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [PosMulStrictMono α] :
      PosMulStrictMono (WithBot α)
      source
      theorem WithBot.instMulPosStrictMono {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [MulPosStrictMono α] :
      MulPosStrictMono (WithBot α)
      source
      theorem WithBot.instPosMulReflectLT {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [PosMulReflectLT α] :
      PosMulReflectLT (WithBot α)
      source
      theorem WithBot.instMulPosReflectLT {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [MulPosReflectLT α] :
      MulPosReflectLT (WithBot α)
      source
      theorem WithBot.instPosMulReflectLE {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [PosMulReflectLE α] :
      PosMulReflectLE (WithBot α)
      source
      theorem WithBot.instMulPosReflectLE {α : Type u_1} [DecidableEq α] [MulZeroClass α] [Preorder α] [MulPosReflectLE α] :
      MulPosReflectLE (WithBot α)
      source
      instance WithBot.orderedCommSemiring {α : Type u_1} [DecidableEq α] [CanonicallyOrderedCommSemiring α] [Nontrivial α] :
      OrderedCommSemiring (WithBot α)
      Equations