Theorems · Theorem · group theory

Finset.sum_sigma

∀ {α : Type u_3} {β : Type u_4} [inst : AddCommMonoid β] {σ : α → 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 sum over a sigma type equals the sum of the fiberwise sums. For rewriting in the reverse direction, use Finset.sum_sigma'. See also Fintype.sum_sigma for the sum over the whole type.

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Sigma

Cited by

12 results in Mathlib

Foundations

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

Assumes

AddCommMonoid