coe_smul — Mathlib

English

Let r be an element of R and f an additive monoid endomorphism of A. Then the action of r on f corresponds to applying r to the outputs of f, i.e., (r • f)(a) = r • f(a) for all a ∈ A.

Русский

Пусть r ∈ R и f — конечное по сложению отображение A → A. Тогда действие скаляра r на f соответствует поэлементному применению r к значениям f: (r • f)(a) = r • f(a) для всех a ∈ A.

LaTeX

$$$ \forall r \in R \; \forall f \in \mathrm{End}(A) \; \forall a \in A:\ (r \cdot f)(a) = r \cdot f(a) $$$

Lean4

@[simp]
theorem coe_smul (r : R) (f : AddMonoid.End A) : ⇑(r • f) = r • ⇑f :=
  rfl

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