English
If p ≠ 0, and for all m ≤ n we have (derivative^m p)(t) = 0, and (n.factorial ∈ nonZeroDivisors R), then n < p.rootMultiplicity t.
Русский
Если p ≠ 0 и для всех m ≤ n выполняется (derivative^m p)(t) = 0, а n! ∈ nonZeroDivisors(R), то n < p.rootMultiplicity t.
LaTeX
$$$$n < p.rootMultiplicity\,t\quad\text{если}\quad \forall m\le n,\ (\ derivative^{[m]} p)(t)=0\ \,\&\, n!\in\operatorname{nonZeroDivisors}(R)$$$$
Lean4
theorem lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0)
(hroot : ∀ m ≤ n, (derivative^[m] p).IsRoot t) (hnzd : (n.factorial : R) ∈ nonZeroDivisors R) :
n < p.rootMultiplicity t := by
by_contra! h'
replace hroot := hroot _ h'
simp only [IsRoot, eval_iterate_derivative_rootMultiplicity] at hroot
obtain ⟨q, hq⟩ : ((rootMultiplicity t p)! : R) ∣ n ! := by gcongr
rw [hq, mul_mem_nonZeroDivisors] at hnzd
rw [nsmul_eq_mul, mul_left_mem_nonZeroDivisors_eq_zero_iff hnzd.1] at hroot
exact eval_divByMonic_pow_rootMultiplicity_ne_zero t h hroot
