smul_apply

Mathlib.Algebra.Module.Hom

URI: https://scilib.ai/kg/mathlib#AddMonoid.End.smul_apply

English

For any r ∈ R, f ∈ End(A), and x ∈ A, the evaluation of the smoothed endomorphism satisfies (r • f)(x) = r • f(x).

Русский

Для любых r ∈ R, f ∈ End(A) и x ∈ A верно (r • f)(x) = r • f(x).

LaTeX

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

Lean4

theorem smul_apply (r : R) (f : AddMonoid.End A) (x : A) : (r • f) x = r • f x :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru