of_mem_support_derivative — Mathlib

English

If n lies in the support of the derivative of p, then n + 1 lies in the support of p.

Русский

Если n принадлежит опоре производной p, то n+1 принадлежит опоре p.

LaTeX

$$$n \in \operatorname{supp}(p') \implies n+1 \in \operatorname{supp}(p)$$$

Lean4

theorem of_mem_support_derivative {p : R[X]} {n : ℕ} (h : n ∈ p.derivative.support) : n + 1 ∈ p.support :=
  mem_support_iff.2 fun h1 : p.coeff (n + 1) = 0 =>
    mem_support_iff.1 h <| show p.derivative.coeff n = 0 by rw [coeff_derivative, h1, zero_mul]

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