English
Equivalent statement for sum over Finset: the evaluation of f on a tuple made by finite sums equals the Finset piFinset sum over all functions r of f evaluated at the corresponding pieces.
Русский
Эквивалентное утверждение для суммы по Finset: значение f на кортеж, составленный из конечных сумм, равно сумме по piFinset над всеми функциями r.
LaTeX
$$$ f(\text{instHAdd.hAdd m m'}) = (\text{piFinset}.sum \ r ...) $$$
Lean4
/-- If `f` is continuous alternating, 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 [∀ i, Fintype (α i)] : (f fun i => ∑ j, g' i j) = ∑ r : ∀ i, α i, f fun i => g' i (r i) :=
f.toMultilinearMap.map_sum _
