lt_rootMultiplicity_iff_isRoot_iterate_derivative

English

Let p ∈ R[X], t ∈ R with CharZero R and p ≠ 0. Then n < rootMultiplicity_t(p) if and only if ∀ m ≤ n, (derivative^m p).IsRoot t.

Русский

Пусть p ∈ R[X], t ∈ R, p ≠ 0, char(R)=0. Тогда выполняется эквивалентно: n < ord_t(p) тогда и только тогда, когда ∀ m ≤ n, (d^m p)(t)=0.

LaTeX

$$$p \neq 0 \ \wedge\ [\text{CharZero } R] \implies \Bigl(n < \operatorname{rootMultiplicity}_t(p) \iff \forall m \le n, (\operatorname{derivative}^{\,m} p).IsRoot t\Bigr).$$$

Lean4

theorem lt_rootMultiplicity_iff_isRoot_iterate_derivative [CharZero R] {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0) :
    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 h hr⟩

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