sum_smul — Mathlib

English

For a multiset l of scalars in R and a vector x ∈ M, (l.sum) • x = (l.map (λ r, r • x)).sum.

Русский

Для мультасета l скаляров из R и вектора 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 : Multiset R} {x : M} : l.sum • x = (l.map fun r ↦ r • x).sum :=
  ((smulAddHom R M).flip x).map_multiset_sum l

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