English
Updating a coordinate by c • u scales the image linearly: map(update f i (c•u)) = c • map(update f i u).
Русский
Обновление координаты на (c•u) масштабирует изображение на скаляре c.
LaTeX
$$$\mathrm{map}(\mathrm{update}\ f\ i\ (c \cdot u)) = c \cdot \mathrm{map}(\mathrm{update}\ f\ i\ u)$$$
Lean4
protected theorem map_update_smul [DecidableEq ι] (i : ι) (c : R) (u : s i →ₗ[R] t i) :
map (update f i (c • u)) = c • map (update f i u) := by
ext x
simp only [LinearMap.compMultilinearMap_apply, map_tprod, map_add_smul_aux, LinearMap.smul_apply,
MultilinearMap.map_update_smul]