English
Assume NoZeroSMulDivisors ℕ R. For every p ∈ R[X] and n ∈ ℕ, the membership of n in the support of derivative p exactly corresponds to membership of n+1 in the support of p: n ∈ supp(derivative p) ⇔ n+1 ∈ supp(p).
Русский
Пусть NoZeroSMulDivisors ℕ R. Для любого p ∈ R[X] и n ∈ ℕ принадлежность n в опоре производной p эквивалентна принадлежности n+1 в опоре p: n ∈ supp(derivative p) ⇔ n+1 ∈ supp(p).
LaTeX
$$$$ n \in \operatorname{supp}(\operatorname{derivative} p) \;\iff\; n+1 \in \operatorname{supp}(p) $$$$
Lean4
theorem mem_support_derivative [NoZeroSMulDivisors ℕ R] (p : R[X]) (n : ℕ) :
n ∈ (derivative p).support ↔ n + 1 ∈ p.support :=
by
suffices ¬p.coeff (n + 1) * (n + 1 : ℕ) = 0 ↔ coeff p (n + 1) ≠ 0 by
simpa only [mem_support_iff, coeff_derivative, Ne, Nat.cast_succ]
rw [← nsmul_eq_mul', smul_eq_zero]
simp only [Nat.succ_ne_zero, false_or]
