English
For integers with binomial ring structure, multichoose is defined by a closed form that matches the combinatorial counting interpretation for nonnegative arguments and uses alternating signs for negative integers.
Русский
Для целых чисел с биномиальной структурой multichoose задаётся явной формулой, совмещающей комбинаторную трактовку для неотрицательных аргументов и чередование знаков для отрицательных.
LaTeX
$$$\text{Int}.multichoose(n,k)$ equals the piecewise definition given by Int.multichoose, i.e., with either $\binom{n+k-1}{k}$ or $(-1)^k \binom{n+1}{k}$ depending on n.$$
Lean4
/-- The multichoose function for integers. -/
def multichoose (n : ℤ) (k : ℕ) : ℤ :=
match n with
| ofNat n => (Nat.choose (n + k - 1) k : ℤ)
| negSucc n => Int.negOnePow k * Nat.choose (n + 1) k
