English
The leading coefficient of the preHilbertPoly F d k is (d!)^{-1}.
Русский
Ведущая коэффициента preHilbertPoly F d k равна (d!)^{-1}.
LaTeX
$$$\operatorname{leadingCoeff}\big(\operatorname{preHilbertPoly}(F,d,k)\big) = (d!)^{-1}$$$
Lean4
theorem coeff_preHilbertPoly_self [CharZero F] (d k : ℕ) : (preHilbertPoly F d k).coeff d = (d ! : F)⁻¹ :=
by
delta preHilbertPoly
have hne : (d ! : F) ≠ 0 := by norm_cast; positivity
have heq : d = ((ascPochhammer F d).comp (X - C (k : F) + 1)).natDegree :=
(natDegree_preHilbertPoly F d k).symm.trans (natDegree_smul _ (inv_ne_zero hne))
nth_rw 3 [heq]
calc
_ = (d ! : F)⁻¹ • ((ascPochhammer F d).comp (X - C ((k : F) - 1))).leadingCoeff := by
simp only [sub_add, ← C_1, ← map_sub, coeff_smul, coeff_natDegree]
_ = (d ! : F)⁻¹ := by
simp only [leadingCoeff_comp (ne_of_eq_of_ne (natDegree_X_sub_C _) one_ne_zero),
Monic.def.1 (monic_ascPochhammer _ _), leadingCoeff_X_sub_C, one_pow, smul_eq_mul, mul_one]
