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]
@[simp]
theorem
WithTop.mul_top
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
{a : WithTop α}
(h : a ≠ 0)
:
@[simp]
theorem
WithTop.top_mul
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
{b : WithTop α}
(hb : b ≠ 0)
:
@[simp]
theorem
WithTop.mul_def
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
(a : WithTop α)
(b : WithTop α)
:
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_lt_top'
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
[LT α]
{a : WithTop α}
{b : WithTop α}
(ha : a < ⊤)
(hb : b < ⊤)
:
theorem
WithTop.mul_lt_top
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
[LT α]
{a : WithTop α}
{b : WithTop α}
(ha : a ≠ ⊤)
(hb : b ≠ ⊤)
:
instance
WithTop.instNoZeroDivisors
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
[NoZeroDivisors α]
:
Equations
- ⋯ = ⋯
instance
WithTop.instMulZeroOneClass
{α : Type u_1}
[DecidableEq α]
[MulZeroOneClass α]
[Nontrivial α]
:
Nontrivial α
is needed here as otherwise we have 1 * ⊤ = ⊤
but also 0 * ⊤ = 0
.
Equations
- WithTop.instMulZeroOneClass = let __spread.0 := WithTop.instMulZeroClass; MulZeroOneClass.mk ⋯ ⋯
@[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)
:
⇑(MonoidWithZeroHom.withTopMap f hf) = WithTop.map ⇑f
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)
:
A version of WithTop.map
for MonoidWithZeroHom
s.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
WithTop.instSemigroupWithZero
{α : Type u_1}
[DecidableEq α]
[SemigroupWithZero α]
[NoZeroDivisors α]
:
Equations
- WithTop.instSemigroupWithZero = let __spread.0 := WithTop.instMulZeroClass; SemigroupWithZero.mk ⋯ ⋯
instance
WithTop.instMonoidWithZero
{α : Type u_1}
[DecidableEq α]
[MonoidWithZero α]
[NoZeroDivisors α]
[Nontrivial α]
:
Equations
- WithTop.instMonoidWithZero = let __spread.0 := WithTop.instMulZeroOneClass; let __spread.1 := WithTop.instSemigroupWithZero; MonoidWithZero.mk ⋯ ⋯
@[simp]
theorem
WithTop.coe_pow
{α : Type u_1}
[DecidableEq α]
[MonoidWithZero α]
[NoZeroDivisors α]
[Nontrivial α]
(a : α)
(n : ℕ)
:
instance
WithTop.instCommMonoidWithZero
{α : Type u_1}
[DecidableEq α]
[CommMonoidWithZero α]
[NoZeroDivisors α]
[Nontrivial α]
:
Equations
- WithTop.instCommMonoidWithZero = let __spread.0 := WithTop.instMonoidWithZero; 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 = let __src := WithTop.addCommMonoidWithOne; let __src_1 := WithTop.instCommMonoidWithZero; CommSemiring.mk ⋯
instance
WithTop.instCanonicallyOrderedCommSemiringWithTop
{α : Type u_1}
[DecidableEq α]
[CanonicallyOrderedCommSemiring α]
[Nontrivial α]
:
Equations
- One or more equations did not get rendered due to their size.
@[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)
:
⇑(RingHom.withTopMap f hf) = (MonoidWithZeroHom.withTopMap (RingHom.toMonoidWithZeroHom f) hf).toFun
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)
:
A version of WithTop.map
for RingHom
s.
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
WithBot.instMulZeroClassWithBot
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
:
MulZeroClass (WithBot α)
Equations
- WithBot.instMulZeroClassWithBot = WithTop.instMulZeroClass
@[simp]
@[simp]
theorem
WithBot.mul_bot
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
{a : WithBot α}
(h : a ≠ 0)
:
@[simp]
theorem
WithBot.bot_mul
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
{b : WithBot α}
(hb : b ≠ 0)
:
@[simp]
theorem
WithBot.mul_def
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
(a : WithBot α)
(b : WithBot α)
:
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.bot_lt_mul'
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
[LT α]
{a : WithBot α}
{b : WithBot α}
(ha : ⊥ < a)
(hb : ⊥ < b)
:
theorem
WithBot.bot_lt_mul
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
[LT α]
{a : WithBot α}
{b : WithBot α}
(ha : a ≠ ⊥)
(hb : b ≠ ⊥)
:
instance
WithBot.instNoZeroDivisors
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
[NoZeroDivisors α]
:
Equations
- ⋯ = ⋯
instance
WithBot.instMulZeroOneClass
{α : Type u_1}
[DecidableEq α]
[MulZeroOneClass α]
[Nontrivial α]
:
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 α]
:
Equations
- WithBot.instSemigroupWithZero = WithTop.instSemigroupWithZero
instance
WithBot.instMonoidWithZero
{α : Type u_1}
[DecidableEq α]
[MonoidWithZero α]
[NoZeroDivisors α]
[Nontrivial α]
:
Equations
- WithBot.instMonoidWithZero = WithTop.instMonoidWithZero
@[simp]
theorem
WithBot.coe_pow
{α : Type u_1}
[DecidableEq α]
[MonoidWithZero α]
[NoZeroDivisors α]
[Nontrivial α]
(a : α)
(n : ℕ)
:
instance
WithBot.commMonoidWithZero
{α : Type u_1}
[DecidableEq α]
[CommMonoidWithZero α]
[NoZeroDivisors α]
[Nontrivial α]
:
Equations
- WithBot.commMonoidWithZero = WithTop.instCommMonoidWithZero
instance
WithBot.commSemiring
{α : Type u_1}
[DecidableEq α]
[CanonicallyOrderedCommSemiring α]
[Nontrivial α]
:
CommSemiring (WithBot α)
Equations
- WithBot.commSemiring = WithTop.commSemiring
instance
WithBot.instPosMulMonoWithBotToMulInstMulZeroClassWithBotZeroToZeroPreorder
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
[Preorder α]
[PosMulMono α]
:
PosMulMono (WithBot α)
Equations
- ⋯ = ⋯
instance
WithBot.instMulPosMonoWithBotToMulInstMulZeroClassWithBotZeroToZeroPreorder
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
[Preorder α]
[MulPosMono α]
:
MulPosMono (WithBot α)
Equations
- ⋯ = ⋯
instance
WithBot.instPosMulStrictMonoWithBotToMulInstMulZeroClassWithBotZeroToZeroPreorder
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
[Preorder α]
[PosMulStrictMono α]
:
Equations
- ⋯ = ⋯
instance
WithBot.instMulPosStrictMonoWithBotToMulInstMulZeroClassWithBotZeroToZeroPreorder
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
[Preorder α]
[MulPosStrictMono α]
:
Equations
- ⋯ = ⋯
instance
WithBot.instPosMulReflectLTWithBotToMulInstMulZeroClassWithBotZeroToZeroPreorder
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
[Preorder α]
[PosMulReflectLT α]
:
Equations
- ⋯ = ⋯
instance
WithBot.instMulPosReflectLTWithBotToMulInstMulZeroClassWithBotZeroToZeroPreorder
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
[Preorder α]
[MulPosReflectLT α]
:
Equations
- ⋯ = ⋯
instance
WithBot.instPosMulReflectLEWithBotToMulInstMulZeroClassWithBotZeroToZeroPreorder
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
[Preorder α]
[PosMulReflectLE α]
:
Equations
- ⋯ = ⋯
instance
WithBot.instMulPosReflectLEWithBotToMulInstMulZeroClassWithBotZeroToZeroPreorder
{α : Type u_1}
[DecidableEq α]
[MulZeroClass α]
[Preorder α]
[MulPosReflectLE α]
:
Equations
- ⋯ = ⋯
instance
WithBot.orderedCommSemiring
{α : Type u_1}
[DecidableEq α]
[CanonicallyOrderedCommSemiring α]
[Nontrivial α]
:
Equations
- WithBot.orderedCommSemiring = let __src := ⋯; let __src := WithBot.orderedAddCommMonoid; let __src_1 := WithBot.commSemiring; OrderedCommSemiring.mk ⋯