Documentation

Mathlib.Algebra.Order.Monoid.ToMulBot

Making an additive monoid multiplicative then adding a zero is the same as adding a bottom element then making it multiplicative.

source
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
Instances For
    source
    @[simp]
    theorem WithZero.toMulBot_zero {α : Type u} [Add α] :
    WithZero.toMulBot 0 = Multiplicative.ofAdd ⊥
    source
    @[simp]
    theorem WithZero.toMulBot_coe {α : Type u} [Add α] (x : Multiplicative α) :
    WithZero.toMulBot ↑x = Multiplicative.ofAdd ↑(Multiplicative.toAdd x)
    source
    @[simp]
    theorem WithZero.toMulBot_symm_bot {α : Type u} [Add α] :
    (MulEquiv.symm WithZero.toMulBot) (Multiplicative.ofAdd ⊥) = 0
    source
    @[simp]
    theorem WithZero.toMulBot_coe_ofAdd {α : Type u} [Add α] (x : α) :
    (MulEquiv.symm WithZero.toMulBot) (Multiplicative.ofAdd ↑x) = ↑(Multiplicative.ofAdd x)
    source
    theorem WithZero.toMulBot_strictMono {α : Type u} [Add α] [Preorder α] :
    StrictMono ⇑WithZero.toMulBot
    source
    @[simp]
    theorem WithZero.toMulBot_le {α : Type u} [Add α] [Preorder α] (a : WithZero (Multiplicative α)) (b : WithZero (Multiplicative α)) :
    WithZero.toMulBot a ≤ WithZero.toMulBot b ↔ a ≤ b
    source
    @[simp]
    theorem WithZero.toMulBot_lt {α : Type u} [Add α] [Preorder α] (a : WithZero (Multiplicative α)) (b : WithZero (Multiplicative α)) :
    WithZero.toMulBot a < WithZero.toMulBot b ↔ a < b