English
The cardinality of piFinset with a constant function equals the same as above with card(s) raised to n.
Русский
Кардинальность piFinset константной функции равна соответствующему выражению кардинальности s возведённому в n.
LaTeX
$$$\\#(\\mathrm{piFinset}\\, (\\lambda _ : \\mathrm{Fin}\\ n \\mapsto s)) = \\#s^n$$$
Lean4
/-- Product over a sigma type equals the repeated product.
This is a version of `Finset.prod_sigma` specialized to the case
of multiplication over `Finset.univ`. -/
@[to_additive /-- Sum over a sigma type equals the repeated sum.
This is a version of `Finset.sum_sigma` specialized to the case of summation over `Finset.univ`. -/
]
theorem prod_sigma {ι} {α : ι → Type*} {M : Type*} [Fintype ι] [∀ i, Fintype (α i)] [CommMonoid M] (f : Sigma α → M) :
∏ x, f x = ∏ x, ∏ y, f ⟨x, y⟩ :=
Finset.prod_sigma ..
