English
If p ≠ 0 and d > rootMultiplicity 1, then (hilbertPoly p d).natDegree = d - rootMultiplicity 1 - 1.
Русский
Если p ≠ 0 и d > rootMultiplicity 1, то natDegree hilbertPoly p d равен d - rootMultiplicity 1 - 1.
LaTeX
$$$\text{If } p \neq 0 \text{ and } d > p.rootMultiplicity 1, \; \operatorname{natDegree}(\operatorname{hilbertPoly}(p, d)) = d - p.rootMultiplicity 1 - 1$$$
Lean4
theorem natDegree_hilbertPoly_of_ne_zero_of_rootMultiplicity_lt {p : F[X]} {d : ℕ} (hp : p ≠ 0)
(hpd : p.rootMultiplicity 1 < d) : (hilbertPoly p d).natDegree = d - p.rootMultiplicity 1 - 1 :=
by
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 _ _)
nth_rw 1 [heq, ← Nat.sub_add_cancel (le_of_lt hpd), hilbertPoly_mul_one_sub_pow_add, ←
Nat.sub_add_cancel (Nat.le_sub_of_add_le' <| add_one_le_of_lt hpd)]
delta hilbertPoly
apply natDegree_eq_of_le_of_coeff_ne_zero
· apply natDegree_sum_le_of_forall_le _ _ <| fun _ _ => ?_
apply le_trans (natDegree_smul_le _ _)
rw [natDegree_preHilbertPoly]
· have : (fun (x : ℕ) (a : F) => a) = fun x a => a * 1 ^ x := by simp only [one_pow, mul_one]
simp only [finset_sum_coeff, coeff_smul, smul_eq_mul, coeff_preHilbertPoly_self, ← Finset.sum_mul,
← sum_def _ (fun _ a => a), this, ← eval_eq_sum, eval_mul, eval_pow, eval_neg, eval_one, _root_.mul_eq_zero,
pow_eq_zero_iff', neg_eq_zero, one_ne_zero, ne_eq, false_and, or_false, inv_eq_zero, cast_eq_zero, not_or]
exact ⟨(not_iff_not.2 dvd_iff_isRoot).1 hq2, factorial_ne_zero _⟩
