Theorems · Theorem · ring theory

Finset.prod_univ_sum

∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] [inst_1 : DecidableEq ι] {κ : ι → Type u_5} [inst_2 : Fintype ι]
  (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ i → R), ∏ i, ∑ j ∈ t i, f i j = ∑ x ∈ Fintype.piFinset t, ∏ i, f i (x i)

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.

Defined in

Mathlib.Algebra.BigOperators.Ring.Finset

Cited by

6 results in Mathlib

Foundations

Depth 78 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringDecidableEqFintype