English
For any r and n, choose (−r) n equals (−1)^n times choose (r+n−1) n.
Русский
Для любого r и n выполняется choose(−r) n = (−1)^n · choose (r+n−1) n.
LaTeX
$$$ \forall R\ [NonAssocRing\ R]\ [Pow\ R\ Nat]\ [BinomialRing\ R]\ (r: R)\ (n:\mathbb{N}),\ choose(-r) n = (-1)^n \cdot choose(r+n-1) n$$$
Lean4
theorem choose_neg [NatPowAssoc R] (r : R) (n : ℕ) : choose (-r) n = Int.negOnePow n • choose (r + n - 1) n :=
by
apply (nsmul_right_inj (Nat.factorial_ne_zero n)).mp
rw [← descPochhammer_eq_factorial_smul_choose, smul_comm, ← descPochhammer_eq_factorial_smul_choose,
descPochhammer_smeval_eq_ascPochhammer, show (-r - n + 1) = -(r + n - 1) by abel,
ascPochhammer_smeval_neg_eq_descPochhammer]
