English
There is a natural isomorphism MonoidHom α β ≃ AddMonoidHom (Additive α) (Additive β).
Русский
Существует естественное изоморфное отображение MonoidHom α β ≃ AddMonoidHom (Additive α) (Additive β).
LaTeX
$$$\text{MonoidHom }(\alpha, \beta) \simeq \text{AddMonoidHom}(\mathrm{Additive}\alpha, \mathrm{Additive}\beta)$$$
Lean4
/-- Reinterpret `α →* β` as `Additive α →+ Additive β`. -/
@[simps]
def toAdditive [MulOneClass α] [MulOneClass β] : (α →* β) ≃ (Additive α →+ Additive β)
where
toFun
f :=
{ toFun := fun a => ofMul (f a.toMul)
map_add' := f.map_mul
map_zero' := f.map_one }
invFun
f :=
{ toFun := fun a => (f (ofMul a)).toMul
map_mul' := f.map_add
map_one' := f.map_zero }
