English
If f is multilinear, then the sum over i of sums over A_i equals the sum over all index functions r in the product Finset of A, of f evaluated at the coordinates g i (r i).
Русский
Если f мультиленейная, то сумма по i сумм по A_i равна сумме по всем функциям r в произведении Finset A над значениями f на координатах g i (r i).
LaTeX
$$$ f ( \\lambda i, \\sum_{j \\in A i} g i j ) = \\sum r \\in \\piFinset A, f ( \\lambda i, g i (r i) ) $$$
Lean4
/-- If `f` is multilinear, then `f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ)` is the sum of
`f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions with `r 1 ∈ A₁`, ...,
`r n ∈ Aₙ`. This follows from multilinearity by expanding successively with respect to each
coordinate. -/
theorem map_sum_finset [DecidableEq ι] [Fintype ι] :
(f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i) :=
f.map_sum_finset_aux _ _ rfl
