Theorems · Theorem · ring theory

Finset.prod_sum

∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] [inst_1 : DecidableEq ι] {κ : ι → Type u_5} (s : Finset ι)
  (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ i → R),
  ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)

The product over a sum can be written as a sum over the product of sets, Finset.Pi. Finset.prod_univ_sum is an alternative statement when the product is over univ.

Defined in

Mathlib.Algebra.BigOperators.Ring.Finset

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiringDecidableEq