English
There is an equivalence AddMonoidHom α (Additive β) ≃ MonoidHom (Multiplicative α) β, implemented by mapping f to a → f(a.toAdd).toMul.
Русский
Существует эквивалентность AddMonoidHom α (Additive β) ≃ MonoidHom (Multiplicative α) β, заданная отображением f ↦ (a → f(a.toAdd)).toMul.
LaTeX
$$$\text{AddMonoidHom}(\alpha, \mathrm{Additive}\beta) \simeq \text{MonoidHom}(\mathrm{Multiplicative}\alpha, \beta)$$$
Lean4
/-- Reinterpret `α →+ Additive β` as `Multiplicative α →* β`. -/
@[simps]
def toMultiplicativeLeft [AddZeroClass α] [MulOneClass β] : (α →+ Additive β) ≃ (Multiplicative α →* β)
where
toFun
f :=
{ toFun := fun a => (f a.toAdd).toMul
map_mul' := f.map_add
map_one' := f.map_zero }
invFun
f :=
{ toFun := fun a => ofMul (f (ofAdd a))
map_add' := f.map_mul
map_zero' := f.map_one }
