English
As a consequence of the auxiliary lemma, the sum over i of sums over A_i equals the piFinset sum of f over the coordinates g i j.
Русский
Следствие из вспомогательной леммы: сумма по i и суммам по A_i равна piFinset-выбору f над координатами g i j.
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₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ)` is the sum of
`f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions `r`. This follows from
multilinearity by expanding successively with respect to each coordinate. -/
theorem map_sum [DecidableEq ι] [Fintype ι] [∀ i, Fintype (α i)] :
(f fun i => ∑ j, g i j) = ∑ r : ∀ i, α i, f fun i => g i (r i) :=
f.map_sum_finset g fun _ => Finset.univ
