English
The derivative of expanded f by p satisfies a product rule with X^{p-1}:
Русский
Производная от расширенного по p полинома удовлетворяет правилу произведения с X^{p-1}:
LaTeX
$$$\operatorname{derivative}(\operatorname{expand}(R,p) f) = \operatorname{expand}(R,p)(\operatorname{derivative} f) \cdot \bigl(p \cdot X^{p-1}\bigr)$$$
Lean4
theorem derivative_expand (f : R[X]) :
Polynomial.derivative (expand R p f) = expand R p (Polynomial.derivative f) * (p * (X ^ (p - 1) : R[X])) := by
rw [coe_expand, derivative_eval₂_C, derivative_pow, C_eq_natCast, derivative_X, mul_one]