map_update_smul — Mathlib

English

Updating at i by scalar multiple r x pulls out the scalar: f(update v i (r x)) = r f(update v i x).

Русский

Обновление на i через r • x выносит скаляр: f(update v i (r x)) = r · f(update v i x).

LaTeX

$$map_update_smul [DecidableEq ι] (i : ι) (r : R) (x : M) : f (update v i (r • x)) = r • f (update v i x)$$

Lean4

@[simp]
theorem map_update_smul [DecidableEq ι] (i : ι) (r : R) (x : M) : f (update v i (r • x)) = r • f (update v i x) :=
  f.map_update_smul' v i r x

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