derivative_comp_one_sub_X — Mathlib

English

For polynomials p and q, derivative(p ∘ q) = derivative(q) · derivative(p) ∘ q.

Русский

Для многочленов p и q производная от p ∘ q равна производной q, умноженной на производную p, применённую к q.

LaTeX

$$$\operatorname{derivative}(p \circ q) = (\operatorname{derivative} q) \cdot (\operatorname{derivative} p) \circ q$$$

Lean4

theorem derivative_comp_one_sub_X (p : R[X]) : derivative (p.comp (1 - X)) = -p.derivative.comp (1 - X) := by
  simp [derivative_comp]

Похожие утверждения