sum_smul — Mathlib

English

For a finite set s ⊆ ι, a function f: ι → R and x ∈ M, the sum of f over s smul x equals the sum over s of f(i) smul x.

Русский

Пусть s ⊆ ι, f: ι → R и x ∈ M. Тогда сумма по i∈s f(i) умножает x так же, как сумма по i∈s f(i) · x.

LaTeX

$$$$ \\left( \\sum_{i \\in s} f(i) \\right) \\cdot x = \\sum_{i \\in s} f(i) \\cdot x. $$$$

Lean4

theorem sum_smul {f : ι → R} {s : Finset ι} {x : M} : (∑ i ∈ s, f i) • x = ∑ i ∈ s, f i • x :=
  map_sum ((smulAddHom R M).flip x) f s

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