English
There is a multiplicative to additive endomorphism equivalence between a monoid endomorphism of M and an additive endomorphism of Additive M; the map respects multiplication.
Русский
Существует эквивалентность между моноидными эндоморфизмами M и аддитивными эндоморфизмами Additive M; отображение сохраняет умножение.
LaTeX
$$$\\operatorname{MonoidEnd}(M) \\simeq \\operatorname{AddMonoidEnd}(\\operatorname{Additive} M)$$$
Lean4
/-- Multiplicative equivalence between multiplicative endomorphisms of a `MulOneClass` `M`
and additive endomorphisms of `Additive M`. -/
@[simps!]
def monoidEndToAdditive (M : Type*) [MulOneClass M] : Monoid.End M ≃* AddMonoid.End (Additive M) :=
{ MonoidHom.toAdditive with map_mul' := fun _ _ => rfl }
