card — Mathlib

English

In the case n = 2, the symmetric square card is the stars-and-bars number: |Sym2 α| = (|α| + 1) choose 2.

Русский

В случае n = 2 кардинал симметрического квадрата равен числу звезд и палок: |Sym2 α| = (|α| + 1) выбирается 2.

LaTeX

$$$|\mathrm{Sym}^2(\alpha)| = \binom{|\alpha|+1}{2}$$$

Lean4

/-- Type **stars and bars** for the case `n = 2`. -/
protected theorem card {α} [Fintype α] : card (Sym2 α) = Nat.choose (card α + 1) 2 :=
  Finset.card_sym2 _

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