English
For p ≠ 0 and under the factorial nonzero divisor condition, n < p.rootMultiplicity t iff all derivative iterates up to n vanish at t.
Русский
При p ≠ 0 и условии, что n! не делит ноль, неравенство n < p.rootMultiplicity t эквивалентно тому, что все итерации производной до n обращаются в ноль в t.
LaTeX
$$$$n < p.rootMultiplicity\,t \iff \forall m \le n, (\text{derivative}^{[m]} p)(t)=0$$$$
Lean4
theorem lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0)
(hnzd : (n.factorial : R) ∈ nonZeroDivisors R) : n < p.rootMultiplicity t ↔ ∀ m ≤ n, (derivative^[m] p).IsRoot t :=
⟨fun hn _ hm ↦ isRoot_iterate_derivative_of_lt_rootMultiplicity <| hm.trans_lt hn, fun hr ↦
lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors h hr hnzd⟩
