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_zero {α : Type u} [Add α] : WithZero.toMulBot 0 = Multiplicative.ofAdd ⊥

@[simp]

theorem WithZero.toMulBot_coe {α : Type u} [Add α] (x : Multiplicative α) : WithZero.toMulBot ↑x = Multiplicative.ofAdd ↑(Multiplicative.toAdd x)

@[simp]

theorem WithZero.toMulBot_symm_bot {α : Type u} [Add α] : WithZero.toMulBot.symm (Multiplicative.ofAdd ⊥) = 0

@[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 b : WithZero (Multiplicative α)) : WithZero.toMulBot a ≤ WithZero.toMulBot b ↔ a ≤ b

@[simp]

theorem WithZero.toMulBot_lt {α : Type u} [Add α] [Preorder α] (a b : WithZero (Multiplicative α)) : WithZero.toMulBot a < WithZero.toMulBot b ↔ a < b