natDegree_preHilbertPoly — Mathlib

English

For any field F and natural numbers d, k, the natural degree of preHilbertPoly F d k equals d; that is, its natDegree is d.

Русский

Для любого поля F и натуральных чисел d, k естественная степень полинома preHilbertPoly F d k равна d; то есть natDegree = d.

LaTeX

$$$\operatorname{natDegree}\big(\operatorname{preHilbertPoly}(F,d,k)\big) = d$$$

Lean4

theorem natDegree_preHilbertPoly [CharZero F] (d k : ℕ) : (preHilbertPoly F d k).natDegree = d :=
  by
  have hne : (d ! : F) ≠ 0 := by norm_cast; positivity
  rw [preHilbertPoly, natDegree_smul _ (inv_ne_zero hne), natDegree_comp, ascPochhammer_natDegree, add_comm_sub, ← C_1,
    ← map_sub, natDegree_add_C, natDegree_X, mul_one]

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