sum_smul — Mathlib

English

For a list l of scalars in R and a vector x in M, the sum of scalars smul x equals the sum of smuls of x by each element: (l.sum) • x = (l.map (λ r, r • x)).sum.

Русский

Для списка l элементов ℝ и вектора x ∈ M выполняется: (l.sum) • x = (l.map (λ r. r • x)).sum.

LaTeX

$$$$ \\left(\\sum l_i\\right) \\cdot x = \\sum_i (l_i \\cdot x). $$$$

Lean4

theorem sum_smul {l : List R} {x : M} : l.sum • x = (l.map fun r ↦ r • x).sum :=
  map_list_sum ((smulAddHom R M).flip x) l

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