English
Let p,q ∈ R[X]. Then the derivative of p.eval₂ C q equals (derivative p).eval₂ C q times derivative q.
Русский
Пусть p,q ∈ R[X]. Тогда производная от p.eval₂ C q равна (derivative p).eval₂ C q умноженному на derivative q.
LaTeX
$$$\operatorname{derivative}\big(p\cdot\mathrm{eval}_2\,C\,q\big) = (\operatorname{derivative} p)\mathrm{eval}_2\,C\,q \cdot \operatorname{derivative} q$$$
Lean4
/-- Chain rule for formal derivative of polynomials. -/
theorem derivative_eval₂_C (p q : R[X]) : derivative (p.eval₂ C q) = p.derivative.eval₂ C q * derivative q :=
Polynomial.induction_on p (fun r => by rw [eval₂_C, derivative_C, eval₂_zero, zero_mul])
(fun p₁ p₂ ih₁ ih₂ => by rw [eval₂_add, derivative_add, ih₁, ih₂, derivative_add, eval₂_add, add_mul]) fun n r ih =>
by
rw [pow_succ, ← mul_assoc, eval₂_mul, eval₂_X, derivative_mul, ih, @derivative_mul _ _ _ X, derivative_X, mul_one,
eval₂_add, @eval₂_mul _ _ _ _ X, eval₂_X, add_mul, mul_right_comm]
