card_sym_eq_multichoose — Mathlib

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 α))

Похожие утверждения