English
The product over all indices of a sum can be rewritten as a sum over all functions from indices to the corresponding finite sets, of the product over indices of the chosen elements.
Русский
Произведение по всем индексам суммы можно переписать как сумму по всем функциям, сопоставляющим индексу элемент из соответствующего множества, от произведения выбранных элементов.
LaTeX
$$$\\prod_{i} \\sum_{j\\in t(i)} f(i,j) = \\sum_{x\\in \\prod_i t(i)} \\prod_i f(i, x(i))$$$
Lean4
/-- The product over `univ` of a sum can be written as a sum over the product of sets,
`Fintype.piFinset`. `Finset.prod_sum` is an alternative statement when the product is not
over `univ`. -/
theorem prod_univ_sum {κ : ι → Type*} [Fintype ι] (t : ∀ i, Finset (κ i)) (f : ∀ i, κ i → R) :
∏ i, ∑ j ∈ t i, f i j = ∑ x ∈ piFinset t, ∏ i, f i (x i) := by
simp only [prod_attach_univ, prod_sum, Finset.sum_univ_pi]
