coe_smul — Mathlib

English

The function corresponding to a scalar action agrees with applying the scalar to the function: the map is linear over the scalar action in the argument.

Русский

Функция, соответствующая скалярному действию, совпадает с применением скаляра к функции: отображение линейно по скаляру в аргументе.

LaTeX

$$$\big( a \cdot f \big) = a \cdot f$ as functions, i.e. $\forall x, (a \cdot f) x = a \cdot f x$$$

Lean4

@[simp]
theorem coe_smul (a : M) (f : E →ₗ.[R] F) : ⇑(a • f) = a • ⇑f :=
  rfl

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