Products over univ.pi

theorem Finset.prod_univ_pi {ι : Type u_1} {β : Type u_2} [CommMonoid β] [DecidableEq ι] [Fintype ι] {κ : ι → Type u_3} (t : (i : ι) → Finset (κ i)) (f : ((i : ι) → i ∈ univ → κ i) → β) : ∏ x ∈ univ.pi t, f x = ∏ x ∈ Fintype.piFinset t, f fun (a : ι) (x_1 : a ∈ univ) => x a

Taking a product over univ.pi t is the same as taking the product 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).

theorem Finset.sum_univ_pi {ι : Type u_1} {β : Type u_2} [AddCommMonoid β] [DecidableEq ι] [Fintype ι] {κ : ι → Type u_3} (t : (i : ι) → Finset (κ i)) (f : ((i : ι) → i ∈ univ → κ i) → β) : ∑ x ∈ univ.pi t, f x = ∑ x ∈ Fintype.piFinset t, f fun (a : ι) (x_1 : a ∈ univ) => 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).