leadingCoeff_preHilbertPoly — Mathlib

English

The coefficient of degree d in the preHilbertPoly F d k is (d!)^{-1}.

Русский

Коэффициент при степени d в preHilbertPoly F d k равен (d!)^{-1}.

LaTeX

$$$\big(\operatorname{coeff}\big(\operatorname{preHilbertPoly}(F,d,k)\big)\big)_{d} = (d!)^{-1}$$$

Lean4

theorem leadingCoeff_preHilbertPoly [CharZero F] (d k : ℕ) : (preHilbertPoly F d k).leadingCoeff = (d ! : F)⁻¹ := by
  rw [leadingCoeff, natDegree_preHilbertPoly, coeff_preHilbertPoly_self]

Похожие утверждения