English
For f : ι →₀ Finset α, the cardinality of f.pi equals the product of the cardinalities of f(i) over i.
Русский
Для f : ι →₀ Finset α, кардинал f.pi равен произведению кардиналов f(i).
LaTeX
$$$|f.pi| = \\prod_{i} |f(i)|$$$
Lean4
@[simp]
theorem card_pi (f : ι →₀ Finset α) : #f.pi = f.prod fun i ↦ #(f i) :=
by
rw [pi, card_finsupp]
exact Finset.prod_congr rfl fun i _ => by simp only [Pi.natCast_apply, Nat.cast_id]