ofEndHom — Mathlib

English

The additive action induced by a hom to Additive End α gives an AddAction M α via [AddAction.ofEndHom f].

Русский

Добавляющее действие, индуцированное гомоморфизмом в AddEnd(α), задаёт AddAction M α через [AddAction.ofEndHom f].

LaTeX

$$$\forall f : M \to_+ \mathrm{AddEnd}(\alpha), \; \mathrm{AddAction.ofEndHom}(f) : \mathrm{AddAction} M \alpha.$$$

Lean4

/-- The additive action induced by a hom to `Additive (Function.End α)`

See note [reducible non-instances]. -/
abbrev ofEndHom (f : M →+ Additive (Function.End α)) : AddAction M α :=
  .compHom α f

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