English
The multichoose function is defined as a generalization of binomial coefficients: multichoose r n equals the binomial-like count allowing repetition.
Русский
Функция multichoose обобщает биномиальные коэффициенты: multichoose r n — число вариантов выбора с повторениями, аналогично подсчёту множеств с повторениями.
LaTeX
$$$\operatorname{multichoose}(r,n) = \text{BinomialRing.multichoose}(r,n)$$$
Lean4
/-- The multichoose function is the quotient of ascending Pochhammer evaluation by the corresponding
factorial. When applied to natural numbers, `multichoose k n` describes choosing a multiset of `n`
items from a type of size `k`, i.e., choosing with replacement. -/
def multichoose (r : R) (n : ℕ) : R :=
BinomialRing.multichoose r n
