map_update_smul — Mathlib

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]

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