English
The derivative of a polynomial p is given by the standard sum expression, i.e. derivative p = sum over n of (coeff p n) n X^{n-1}.
Русский
Производная многочлена p задаётся стандартной суммной формулой: derivative p = ∑_n (coeff p n) · n · X^{n-1}.
LaTeX
$$$\\operatorname{derivative}(p) = \\sum_{n \\ge 0} \\operatorname{coeff}(p,n) \\; n \\; X^{n-1}.$$$
Lean4
/-- `derivative p` is the formal derivative of the polynomial `p` -/
def derivative : R[X] →ₗ[R] R[X]
where
toFun p := p.sum fun n a => C (a * n) * X ^ (n - 1)
map_add' p
q := by rw [sum_add_index] <;> simp only [add_mul, forall_const, RingHom.map_add, zero_mul, RingHom.map_zero]
map_smul' a
p := by dsimp;
rw [sum_smul_index] <;>
simp only [mul_sum, ← C_mul', mul_assoc, RingHom.map_mul, forall_const, zero_mul, RingHom.map_zero, sum]
