prod_sum — Mathlib

English

A product over i of a sum over j of f(i,j) equals a sum over all functions x: i↦κ_i of the product over i of f(i, x(i)).

Русский

Произведение по i от суммы по j от f(i,j) равняется сумме по всем функциям x: i↦κ_i от произведения f(i, x(i)).

LaTeX

$$$\\prod_{i} \\sum_{j} f(i,j) = \\sum_{x} \\prod_{i} f(i, x(i))$$$

Lean4

/-- A product of sums can be written as a sum of products. -/
theorem prod_sum {κ : ι → Type*} [∀ i, Fintype (κ i)] (f : ∀ i, κ i → R) :
    ∏ i, ∑ j, f i j = ∑ x : ∀ i, κ i, ∏ i, f i (x i) :=
  Finset.prod_univ_sum _ _

Похожие утверждения