Making an additive monoid multiplicative then adding a zero is the same as adding a bottom element then making it multiplicative.
Making an additive monoid multiplicative then adding a zero is the same as adding a bottom element then making it multiplicative.
Equations
Instances For
@[simp]
@[simp]
@[simp]
theorem
WithZero.toMulBot_le
{α : Type u}
[Add α]
[Preorder α]
(a b : WithZero (Multiplicative α))
:
@[simp]
theorem
WithZero.toMulBot_lt
{α : Type u}
[Add α]
[Preorder α]
(a b : WithZero (Multiplicative α))
: