English
The binomial coefficient for a ring element r and natural n is defined as the multichoose of (r − n + 1) and n, i.e., choose r n = multichoose (r − n + 1) n.
Русский
Биномный коэффициент для элемента кольца r и натурального n определяется как multichoose (r − n + 1) n, то есть choose r n = multichoose (r − n + 1) n.
LaTeX
$$$ \text{choose } : R \times \mathbb{N} \to R,\quad \text{choose } r\, n = \operatorname{multichoose}(r - n + 1,\, n)$$$
Lean4
/-- The binomial coefficient `choose r n` generalizes the natural number `Nat.choose` function,
interpreted in terms of choosing without replacement. -/
def choose [AddCommGroupWithOne R] [Pow R ℕ] [BinomialRing R] (r : R) (n : ℕ) : R :=
multichoose (r - n + 1) n
