English
For any polynomial p and natural n, the coefficient of derivative p at n equals coeff(p, n+1) times (n+1).
Русский
Для любого p и натурала n коэффициент производной p при индексе n равен coeff(p, n+1) · (n+1).
LaTeX
$$$\\operatorname{coeff}(\\operatorname{derivative}(p),n) = \\operatorname{coeff}(p,n+1) \\cdot (n+1).$$$
Lean4
theorem coeff_derivative (p : R[X]) (n : ℕ) : coeff (derivative p) n = coeff p (n + 1) * (n + 1) :=
by
rw [derivative_apply]
simp only [coeff_X_pow, coeff_sum, coeff_C_mul]
rw [sum, Finset.sum_eq_single (n + 1)]
· simp only [Nat.add_succ_sub_one, add_zero, mul_one, if_true]; norm_cast
· intro b
cases b
· intros
rw [Nat.cast_zero, mul_zero, zero_mul]
· intro _ H
rw [Nat.add_one_sub_one, if_neg (mt (congr_arg Nat.succ) H.symm), mul_zero]
· simp_all
