English
For any finite α of cardinality n, the number of multisets of size k from α equals multichoose(n, k).
Русский
Для конечного множества α с кардинальностью n число мультимножеств размера k из α равно multichoose(n, k).
LaTeX
$$$|\mathrm{Sym}(\alpha, k)| = \mathrm{multichoose}\,(|\alpha|,\ k)$$$
Lean4
/-- For any fintype `α` of cardinality `n`, `card (Sym α k) = multichoose (card α) k`. -/
theorem card_sym_eq_multichoose (α : Type*) (k : ℕ) [Fintype α] [Fintype (Sym α k)] :
card (Sym α k) = multichoose (card α) k :=
by
rw [← card_sym_fin_eq_multichoose]
exact card_congr (equivCongr (equivFin α))