multichoose — Mathlib

English

The number of multisets of cardinality k from a set of size n equals C(n+k−1,k).

Русский

Количество мультимножеств размера k из множества размера n равно C(n+k−1,k).

LaTeX

$$$$ \operatorname{multichoose}(n,k) = \binom{n+k-1}{k} $$$$

Lean4

/-- `multichoose n k` is the number of multisets of cardinality `k` from a type of cardinality `n`. -/
def multichoose : ℕ → ℕ → ℕ
  | _, 0 => 1
  | 0, _ + 1 => 0
  | n + 1, k + 1 => multichoose n (k + 1) + multichoose (n + 1) k

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