coe_smul — Mathlib

English

The action of scalars on affine maps is compatible with the evaluation map: the underlying function of c • f is the pointwise scalar action on the function f, i.e., ⇑(c • f) = c • ⇑f.

Русский

Действие скаляра на аффинные отображения согласовано с отображением функции: базовая функция c • f равна точечной подстановке c на функцию f, то есть ⇑(c • f) = c • ⇑f.

LaTeX

$$$\forall c\in R,\ f:\,P_1 \to^{\mathrm{aff}}_k V_2,\quad \bigl(c\cdot f\bigr) = c\cdot f\,\text{as functions}.$$$

Lean4

@[simp, norm_cast]
theorem coe_smul (c : R) (f : P1 →ᵃ[k] V2) : ⇑(c • f) = c • ⇑f :=
  rfl

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