English
In a field of characteristic zero, the binomial coefficient equals (n!)^−1 times the smeval of the descPochhammer ℤ n at a.
Русский
В поле нуль-чарты справедливо choose a n = (n!)^−1 • smeval(descPochhammer ℤ n) a.
LaTeX
$$$ \forall R\ [Field\ R]\ [CharZero\ R]\ {a: R} {n: \mathbb{N}},\ \mathrm{choose}\ a n = (n! )^{-1} \cdot (\ascPochhammer \, \mathbb{Z}\ n).\mathrm{smeval}\ al$$$
Lean4
theorem choose_eq_smul [Field R] [CharZero R] {a : R} {n : ℕ} :
Ring.choose a n = (n.factorial : R)⁻¹ • (descPochhammer ℤ n).smeval a :=
by
rw [Ring.descPochhammer_eq_factorial_smul_choose, ← Nat.cast_smul_eq_nsmul R, inv_smul_smul₀]
simpa using Nat.factorial_ne_zero n
