End — Mathlib

English

There is an isomorphism between Monoid.End M and AddMonoid.End (Additive M) as stated previously.

Русский

Существует изоморфизм между Monoid.End M и AddMonoid.End (Additive M).

LaTeX

$$$\\mathrm{MonoidEnd}(M) \\simeq \\mathrm{AddMonoidEnd}(\\mathrm{Additive} M)$$$

Lean4

/-- `Monoid.End M` is equivalent to `AddMonoid.End (Additive M)`. -/
@[simps! apply]
def End [Monoid M] : Monoid.End M ≃* AddMonoid.End (Additive M)
    where
  __ := MonoidHom.toAdditive
  map_mul' := fun _ _ ↦ rfl

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