English
A variant of the equivalence: p ≠ 0 implies the same iff condition, with a strengthened nonzero divisor criterion.
Русский
Вариант эквивалентности: p ≠ 0 даёт такое же условие, но с усиленным критерием неравенства нулю делителей.
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 : ∀ m ≤ n, m ≠ 0 → (m : R) ∈ nonZeroDivisors R) :
n < p.rootMultiplicity t ↔ ∀ m ≤ n, (derivative^[m] p).IsRoot t :=
⟨fun hn _ hm ↦ isRoot_iterate_derivative_of_lt_rootMultiplicity <| Nat.lt_of_le_of_lt hm hn, fun hr ↦
lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors' h hr hnzd⟩
