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