natDegree_hilbertPoly_of_ne_zero — Mathlib

English

If hilbertPoly p d ≠ 0, then (hilbertPoly p d).natDegree = d - p.rootMultiplicity 1 - 1.

Русский

Если hilbertPoly p d ≠ 0, то его natDegree равен d - rootMultiplicity 1 - 1.

LaTeX

$$$\operatorname{natDegree}(\operatorname{hilbertPoly}(p, d)) = d - p.rootMultiplicity 1 - 1$$$

Lean4

theorem natDegree_hilbertPoly_of_ne_zero {p : F[X]} {d : ℕ} (hh : hilbertPoly p d ≠ 0) :
    (hilbertPoly p d).natDegree = d - p.rootMultiplicity 1 - 1 :=
  by
  have hp : p ≠ 0 := by
    intro h
    rw [h] at hh
    exact hh (hilbertPoly_zero_left d)
  have hpd : p.rootMultiplicity 1 < d := by
    by_contra h
    exact hh (hilbertPoly_eq_zero_of_le_rootMultiplicity_one <| not_lt.1 h)
  exact natDegree_hilbertPoly_of_ne_zero_of_rootMultiplicity_lt hp hpd

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