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.

@[simp]

theorem WithZero.toMulBot_zero {α : Type u} [Add α] : toMulBot 0 = Multiplicative.ofAdd ⊥

@[simp]

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

@[simp]

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

@[simp]

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

theorem WithZero.toMulBot_strictMono {α : Type u} [Add α] [Preorder α] : StrictMono ⇑toMulBot

@[simp]

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

@[simp]

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