Structures involving *
and 0
on WithTop
and WithBot
#
The main results of this section are WithTop.canonicallyOrderedCommSemiring
and
WithBot.orderedCommSemiring
.
instance
WithTop.instDecidableEqWithTop
{α : Type u_1}
[inst : DecidableEq α]
:
DecidableEq (WithTop α)
Equations
- WithTop.instDecidableEqWithTop = instDecidableEqOption
instance
WithTop.instMulZeroClassWithTop
{α : Type u_1}
[inst : DecidableEq α]
[inst : Zero α]
[inst : Mul α]
:
MulZeroClass (WithTop α)
Equations
- One or more equations did not get rendered due to their size.
instance
WithTop.noZeroDivisors
{α : Type u_1}
[inst : DecidableEq α]
[inst : Zero α]
[inst : Mul α]
[inst : NoZeroDivisors α]
:
@[simp]
theorem
WithTop.coe_mul
{α : Type u_1}
[inst : DecidableEq α]
[inst : MulZeroClass α]
{a : α}
{b : α}
:
theorem
WithTop.mul_coe
{α : Type u_1}
[inst : DecidableEq α]
[inst : MulZeroClass α]
{b : α}
(hb : b ≠ 0)
{a : WithTop α}
:
a * ↑b = Option.bind a fun a => some (a * b)
@[simp]
theorem
WithTop.untop'_zero_mul
{α : Type u_1}
[inst : DecidableEq α]
[inst : MulZeroClass α]
(a : WithTop α)
(b : WithTop α)
:
WithTop.untop' 0 (a * b) = WithTop.untop' 0 a * WithTop.untop' 0 b
instance
WithTop.instMulZeroOneClassWithTop
{α : Type u_1}
[inst : DecidableEq α]
[inst : MulZeroOneClass α]
[inst : Nontrivial α]
:
Nontrivial α
is needed here as otherwise we have 1 * ⊤ = ⊤⊤ = ⊤⊤
but also 0 * ⊤ = 0⊤ = 0
.
@[simp]
theorem
MonoidWithZeroHom.withTopMap_apply
{R : Type u_1}
{S : Type u_2}
[inst : MulZeroOneClass R]
[inst : DecidableEq R]
[inst : Nontrivial R]
[inst : MulZeroOneClass S]
[inst : DecidableEq S]
[inst : Nontrivial S]
(f : R →*₀ S)
(hf : Function.Injective ↑f)
:
↑(MonoidWithZeroHom.withTopMap f hf) = WithTop.map ↑f
def
MonoidWithZeroHom.withTopMap
{R : Type u_1}
{S : Type u_2}
[inst : MulZeroOneClass R]
[inst : DecidableEq R]
[inst : Nontrivial R]
[inst : MulZeroOneClass S]
[inst : DecidableEq S]
[inst : 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.
instance
WithTop.instSemigroupWithZeroWithTop
{α : Type u_1}
[inst : DecidableEq α]
[inst : SemigroupWithZero α]
[inst : NoZeroDivisors α]
:
instance
WithTop.monoidWithZero
{α : Type u_1}
[inst : DecidableEq α]
[inst : MonoidWithZero α]
[inst : NoZeroDivisors α]
[inst : Nontrivial α]
:
Equations
- One or more equations did not get rendered due to their size.
instance
WithTop.commMonoidWithZero
{α : Type u_1}
[inst : DecidableEq α]
[inst : CommMonoidWithZero α]
[inst : NoZeroDivisors α]
[inst : Nontrivial α]
:
instance
WithTop.commSemiring
{α : Type u_1}
[inst : DecidableEq α]
[inst : CanonicallyOrderedCommSemiring α]
[inst : Nontrivial α]
:
CommSemiring (WithTop α)
This instance requires CanonicallyOrderedCommSemiring
as it is the smallest class
that derives from both NonAssocNonUnitalSemiring
and CanonicallyOrderedAddMonoid
, both
of which are required for distributivity.
instance
WithTop.instCanonicallyOrderedCommSemiringWithTop
{α : Type u_1}
[inst : DecidableEq α]
[inst : CanonicallyOrderedCommSemiring α]
[inst : Nontrivial α]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
RingHom.withTopMap_apply
{R : Type u_1}
{S : Type u_2}
[inst : CanonicallyOrderedCommSemiring R]
[inst : DecidableEq R]
[inst : Nontrivial R]
[inst : CanonicallyOrderedCommSemiring S]
[inst : DecidableEq S]
[inst : 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_1}
{S : Type u_2}
[inst : CanonicallyOrderedCommSemiring R]
[inst : DecidableEq R]
[inst : Nontrivial R]
[inst : CanonicallyOrderedCommSemiring S]
[inst : DecidableEq S]
[inst : 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.
instance
WithBot.instDecidableEqWithBot
{α : Type u_1}
[inst : DecidableEq α]
:
DecidableEq (WithBot α)
Equations
- WithBot.instDecidableEqWithBot = instDecidableEqOption
instance
WithBot.instMulZeroClassWithBot
{α : Type u_1}
[inst : DecidableEq α]
[inst : Zero α]
[inst : Mul α]
:
MulZeroClass (WithBot α)
Equations
- WithBot.instMulZeroClassWithBot = WithTop.instMulZeroClassWithTop
@[simp]
theorem
WithBot.coe_mul
{α : Type u_1}
[inst : DecidableEq α]
[inst : MulZeroClass α]
{a : α}
{b : α}
:
theorem
WithBot.mul_coe
{α : Type u_1}
[inst : DecidableEq α]
[inst : MulZeroClass α]
{b : α}
(hb : b ≠ 0)
{a : WithBot α}
:
a * ↑b = Option.bind a fun a => some (a * b)
instance
WithBot.instMulZeroOneClassWithBot
{α : Type u_1}
[inst : DecidableEq α]
[inst : MulZeroOneClass α]
[inst : Nontrivial α]
:
Nontrivial α
is needed here as otherwise we have 1 * ⊥ = ⊥⊥ = ⊥⊥
but also = 0 * ⊥ = 0⊥ = 0
.
Equations
- WithBot.instMulZeroOneClassWithBot = WithTop.instMulZeroOneClassWithTop
instance
WithBot.instNoZeroDivisorsWithBotToMulInstMulZeroClassWithBotToZeroZero
{α : Type u_1}
[inst : DecidableEq α]
[inst : MulZeroClass α]
[inst : NoZeroDivisors α]
:
instance
WithBot.instSemigroupWithZeroWithBot
{α : Type u_1}
[inst : DecidableEq α]
[inst : SemigroupWithZero α]
[inst : NoZeroDivisors α]
:
Equations
- WithBot.instSemigroupWithZeroWithBot = WithTop.instSemigroupWithZeroWithTop
instance
WithBot.instMonoidWithZeroWithBot
{α : Type u_1}
[inst : DecidableEq α]
[inst : MonoidWithZero α]
[inst : NoZeroDivisors α]
[inst : Nontrivial α]
:
Equations
- WithBot.instMonoidWithZeroWithBot = WithTop.monoidWithZero
instance
WithBot.commMonoidWithZero
{α : Type u_1}
[inst : DecidableEq α]
[inst : CommMonoidWithZero α]
[inst : NoZeroDivisors α]
[inst : Nontrivial α]
:
Equations
- WithBot.commMonoidWithZero = WithTop.commMonoidWithZero
instance
WithBot.commSemiring
{α : Type u_1}
[inst : DecidableEq α]
[inst : CanonicallyOrderedCommSemiring α]
[inst : Nontrivial α]
:
CommSemiring (WithBot α)
Equations
- WithBot.commSemiring = WithTop.commSemiring
instance
WithBot.instPosMulMonoWithBotToMulInstMulZeroClassWithBotToZeroZeroPreorder
{α : Type u_1}
[inst : DecidableEq α]
[inst : MulZeroClass α]
[inst : Preorder α]
[inst : PosMulMono α]
:
PosMulMono (WithBot α)
instance
WithBot.instMulPosMonoWithBotToMulInstMulZeroClassWithBotToZeroZeroPreorder
{α : Type u_1}
[inst : DecidableEq α]
[inst : MulZeroClass α]
[inst : Preorder α]
[inst : MulPosMono α]
:
MulPosMono (WithBot α)
instance
WithBot.instPosMulStrictMonoWithBotToMulInstMulZeroClassWithBotToZeroZeroPreorder
{α : Type u_1}
[inst : DecidableEq α]
[inst : MulZeroClass α]
[inst : Preorder α]
[inst : PosMulStrictMono α]
:
instance
WithBot.instMulPosStrictMonoWithBotToMulInstMulZeroClassWithBotToZeroZeroPreorder
{α : Type u_1}
[inst : DecidableEq α]
[inst : MulZeroClass α]
[inst : Preorder α]
[inst : MulPosStrictMono α]
:
instance
WithBot.instPosMulReflectLTWithBotToMulInstMulZeroClassWithBotToZeroZeroPreorder
{α : Type u_1}
[inst : DecidableEq α]
[inst : MulZeroClass α]
[inst : Preorder α]
[inst : PosMulReflectLT α]
:
instance
WithBot.instMulPosReflectLTWithBotToMulInstMulZeroClassWithBotToZeroZeroPreorder
{α : Type u_1}
[inst : DecidableEq α]
[inst : MulZeroClass α]
[inst : Preorder α]
[inst : MulPosReflectLT α]
:
instance
WithBot.instPosMulMonoRevWithBotToMulInstMulZeroClassWithBotToZeroZeroPreorder
{α : Type u_1}
[inst : DecidableEq α]
[inst : MulZeroClass α]
[inst : Preorder α]
[inst : PosMulMonoRev α]
:
PosMulMonoRev (WithBot α)
instance
WithBot.instMulPosMonoRevWithBotToMulInstMulZeroClassWithBotToZeroZeroPreorder
{α : Type u_1}
[inst : DecidableEq α]
[inst : MulZeroClass α]
[inst : Preorder α]
[inst : MulPosMonoRev α]
:
MulPosMonoRev (WithBot α)
instance
WithBot.orderedCommSemiring
{α : Type u_1}
[inst : DecidableEq α]
[inst : CanonicallyOrderedCommSemiring α]
[inst : Nontrivial α]
:
Equations
- One or more equations did not get rendered due to their size.