Making an additive monoid multiplicative then adding a zero is the same as adding a bottom element then making it multiplicative.
def
WithZero.toMulBot
{α : Type u}
[Add α]
:
WithZero (Multiplicative α) ≃* Multiplicative (WithBot α)
Making an additive monoid multiplicative then adding a zero is the same as adding a bottom element then making it multiplicative.
Equations
- WithZero.toMulBot = MulEquiv.refl (WithZero (Multiplicative α))
@[simp]
theorem
WithZero.toMulBot_coe
{α : Type u}
[Add α]
(x : Multiplicative α)
:
WithZero.toMulBot ↑x = Multiplicative.ofAdd ↑(Multiplicative.toAdd x)
@[simp]
theorem
WithZero.toMulBot_coe_ofAdd
{α : Type u}
[Add α]
(x : α)
:
WithZero.toMulBot.symm (Multiplicative.ofAdd ↑x) = ↑(Multiplicative.ofAdd x)
theorem
WithZero.toMulBot_strictMono
{α : Type u}
[Add α]
[Preorder α]
:
StrictMono ⇑WithZero.toMulBot
@[simp]
theorem
WithZero.toMulBot_le
{α : Type u}
[Add α]
[Preorder α]
(a : WithZero (Multiplicative α))
(b : WithZero (Multiplicative α))
:
@[simp]
theorem
WithZero.toMulBot_lt
{α : Type u}
[Add α]
[Preorder α]
(a : WithZero (Multiplicative α))
(b : WithZero (Multiplicative α))
: