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
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
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' := ⋯ }
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' := ⋯ }
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
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