lt_rootMultiplicity_of_isRoot_iterate_derivative

English

Let p ∈ R[X] with p ≠ 0 and t ∈ R. If for every m ≤ n, the m-th derivative of p vanishes at t (i.e., t is a root of each derivative up to order n), then n < rootMultiplicity_t(p).

Русский

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

LaTeX

$$$p \neq 0 \ \wedge\ \forall m \le n,\ (\text{derivative}^{\,m} p)(t)=0 \implies n < \operatorname{rootMultiplicity}_t(p).$$$

Lean4

theorem lt_rootMultiplicity_of_isRoot_iterate_derivative [CharZero R] {p : R[X]} {t : R} {n : ℕ} (h : p ≠ 0)
    (hroot : ∀ m ≤ n, (derivative^[m] p).IsRoot t) : n < p.rootMultiplicity t :=
  lt_rootMultiplicity_of_isRoot_iterate_derivative_of_mem_nonZeroDivisors h hroot <|
    mem_nonZeroDivisors_of_ne_zero <| Nat.cast_ne_zero.2 <| by positivity

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