toEndHom — Mathlib

English

The additive action induces an additive monoid hom M →+ Additive (End α): toEndHom [AddAction M α] : M →+ Additive (End α).

Русский

Добавляющее действие индуцирует аддитивный моноид-гомоморфизм M →+ Additive (End α).

LaTeX

$$$\mathrm{toEndHom} : M \to_+ \mathrm{AddEnd}(\alpha), \quad \mathrm{toEndHom}(m)(x) = m \cdot x.$$$

Lean4

/-- The additive monoid hom representing an additive monoid action.

When `M` is a group, see `AddAction.toPermHom`. -/
def toEndHom [AddAction M α] : M →+ Additive (Function.End α) :=
  MulAction.toEndHom.toAdditiveRight

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