Theorems · Theorem · group theory

Finset.sum_univ_pi

∀ {ι : Type u_1} {β : Type u_2} [inst : AddCommMonoid β] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  {κ : ι → Type u_3} (t : (i : ι) → Finset (κ i)) (f : ((i : ι) → i ∈ Finset.univ → κ i) → β),
  ∑ x ∈ Finset.univ.pi t, f x = ∑ x ∈ Fintype.piFinset t, f fun a x_1 => x a

Taking a sum over univ.pi t is the same as taking the sum over Fintype.piFinset t. univ.pi t and Fintype.piFinset t are essentially the same Finset, but differ in the type of their element, univ.pi t is a Finset (Π a ∈ univ, t a) and Fintype.piFinset t is a Finset (Π a, t a).

Defined in

Mathlib.Algebra.BigOperators.Group.Finset.Pi

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidDecidableEqFintype