coeFn_smul — Mathlib

English

The evaluation map commutes with scalar multiplication: the function representation of c • f is c • the function representation of f.

Русский

Оценочная отображение коммутирует со скалярным умножением: представление функции от c•f равно c•представлению функции f.

LaTeX

$$$\\iota(c \\cdot f) = c \\cdot \\iota(f)$$$

Lean4

@[simp]
theorem coeFn_smul (c : 𝕜) (f : lp E p) : ⇑(c • f) = c • ⇑f :=
  rfl

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