English
For CharZero field F and d, k, and any n with k ≤ n, the value of preHilbertPoly F d k at n is the binomial coefficient (n − k + d choose d).
Русский
Для поля F с CharZero и для d, k и любого n при условии k ≤ n значение preHilbertPoly F d k в точке n равно биномиальному коэффициенту (n − k + d choose d).
LaTeX
$$$\big(\operatorname{preHilbertPoly}(F,d,k)\big)(n) = \binom{n - k + d}{d} \quad \text{при } k \le n$$$
Lean4
theorem preHilbertPoly_eq_choose_sub_add [CharZero F] (d : ℕ) {k n : ℕ} (hkn : k ≤ n) :
(preHilbertPoly F d k).eval (n : F) = (n - k + d).choose d :=
by
have : (d ! : F) ≠ 0 := by norm_cast; positivity
calc
_ = (↑d !)⁻¹ * eval (↑(n - k + 1)) (ascPochhammer F d) := by simp [cast_sub hkn, preHilbertPoly]
_ = (n - k + d).choose d := by rw [ascPochhammer_nat_eq_natCast_ascFactorial];
simp [field, ascFactorial_eq_factorial_mul_choose]
