End — Mathlib

English

Analogous to the previous item, with roles reversed between additive and multiplicative endomorphisms.

Русский

Аналогично предыдущему пункту, роли поменяны между аддитивными и умножительными эндоморфизмами.

LaTeX

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

Lean4

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

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