English
Let g be a finitely supported function g: α →₀ R, b ∈ R, and h: α → R → M with h i 0 = 0 for all i. Then summing h over the scaled function b • g is the same as summing h over g with the argument scaled by b: (b • g).sum h = g.sum (λ i a, h i (b * a)).
Русский
Пусть g: α →₀ R имеет конечную опорную поддержку, b ∈ R, и h: α → R → M таково, что h i 0 = 0 для всех i. Тогда сумма по i от h i( b g(i) ) равна сумме по i от h i(b i), то есть (b • g).sum h = g.sum (λ i a, h i (b * a)).
LaTeX
$$$(b \cdot g).sum h = g.sum (\lambda i a. h\, i\,(b * a))$$$
Lean4
theorem sum_smul_index [MulZeroClass R] [AddCommMonoid M] {g : α →₀ R} {b : R} {h : α → R → M} (h0 : ∀ i, h i 0 = 0) :
(b • g).sum h = g.sum fun i a => h i (b * a) :=
Finsupp.sum_mapRange_index h0
