toMonoidEnd — Mathlib

English

Every element r of the monoid M defines a monoid endomorphism of A by a ↦ r • a, and the map r ↦ (a ↦ r • a) is a monoid homomorphism M → End(A).

Русский

Каждый элемент r моноида M задаёт концевой эндоморфизм A по формуле a ↦ r • a, и отображение r ↦ (a ↦ r • a) является гомоморфизмом моноидов M → End(A).

LaTeX

$$$ \exists \phi: M \to^* \mathrm{End}(A), \quad \phi(r)(a) = r \cdot a. $$$

Lean4

/-- Each element of the monoid defines a monoid homomorphism. -/
@[simps]
def toMonoidEnd : M →* Monoid.End A
    where
  toFun := MulDistribMulAction.toMonoidHom A
  map_one' := MonoidHom.ext <| one_smul M
  map_mul' x y := MonoidHom.ext <| mul_smul x y

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