Theorems · Theorem · group theory

Finset.prod_sigma

∀ {α : Type u_3} {β : Type u_4} [inst : CommMonoid β] {σ : α → Type u_6} (s : Finset α) (t : (a : α) → Finset (σ a))
  (f : Sigma σ → β), ∏ x ∈ s.sigma t, f x = ∏ a ∈ s, ∏ s ∈ t a, f ⟨a, s⟩

The product over a sigma type equals the product of the fiberwise products. For rewriting in the reverse direction, use Finset.prod_sigma'. See also Fintype.prod_sigma for the product over the whole type.

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Sigma

Cited by

10 results in Mathlib

Foundations

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

Assumes

CommMonoid