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.

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]
    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 : WithZero (Multiplicative α)) (b : WithZero (Multiplicative α)) :
    WithZero.toMulBot a WithZero.toMulBot b a b
    @[simp]
    theorem WithZero.toMulBot_lt {α : Type u} [Add α] [Preorder α] (a : WithZero (Multiplicative α)) (b : WithZero (Multiplicative α)) :
    WithZero.toMulBot a < WithZero.toMulBot b a < b