addMonoidEndToMultiplicative — Mathlib

English

There is a multiplicative equivalence between additive endomorphisms of an AddZeroClass A and multiplicative endomorphisms of Multiplicative A.

Русский

Существует мультипликативная эквивалентность между аддитивными эйндормоморфизмами A и мультипликативными эйндормоморфизмами Multiplicative A.

LaTeX

$$$\mathrm{AddMonoid.End}(A) \simeq^* \mathrm{Monoid.End}(\mathrm{Multiplicative}A)$$$

Lean4

/-- Multiplicative equivalence between additive endomorphisms of an `AddZeroClass` `A`
and multiplicative endomorphisms of `Multiplicative A`. -/
@[simps!]
def addMonoidEndToMultiplicative (A : Type*) [AddZeroClass A] : AddMonoid.End A ≃* Monoid.End (Multiplicative A) :=
  { AddMonoidHom.toMultiplicative with map_mul' := fun _ _ => rfl }

Похожие утверждения