card_sym_eq_choose — Mathlib

English

The stars and bars formula expresses the symmetric content: card(Sym α k) = (card α + k − 1) choose k.

Русский

Формула «звезды и палки» выражает кардинал симметрических структур: |Sym α k| = (|α| + k − 1) выбрать k.

LaTeX

$$$|\mathrm{Sym}(\alpha, k)| = \binom{|\alpha|+k-1}{k}$$$

Lean4

/-- The *stars and bars* lemma: the cardinality of `Sym α k` is equal to
`Nat.choose (card α + k - 1) k`. -/
theorem card_sym_eq_choose {α : Type*} [Fintype α] (k : ℕ) [Fintype (Sym α k)] :
    card (Sym α k) = (card α + k - 1).choose k := by rw [card_sym_eq_multichoose, Nat.multichoose_eq]

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