hilbertPoly_eq_zero_of_le_rootMultiplicity_one

English

If d ≤ rootMultiplicity of p at 1, then hilbertPoly p d = 0.

Русский

Если d не превосходит кратность корня p в 1, то hilbertPoly p d = 0.

LaTeX

$$$\text{If } d \le p.rootMultiplicity 1, \; \operatorname{hilbertPoly}(p, d) = 0$$$

Lean4

theorem hilbertPoly_eq_zero_of_le_rootMultiplicity_one {p : F[X]} {d : ℕ} (hdp : d ≤ p.rootMultiplicity 1) :
    hilbertPoly p d = 0 := by
  by_cases hp : p = 0
  · rw [hp, hilbertPoly_zero_left]
  · rcases exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp 1 with ⟨q, hq1, hq2⟩
    have heq : p = q * (-1) ^ p.rootMultiplicity 1 * (1 - X) ^ p.rootMultiplicity 1 :=
      by
      simp only [mul_assoc, ← mul_pow, neg_mul, one_mul, neg_sub]
      exact hq1.trans (mul_comm _ _)
    rw [heq, ← zero_add d, ← Nat.sub_add_cancel hdp, pow_add (1 - X), ← mul_assoc, hilbertPoly_mul_one_sub_pow_add,
      hilbertPoly]

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