derivative_comp — Mathlib

English

Let p,q ∈ R[X]. Then the derivative of the composition p ∘ q satisfies (p ∘ q)' = q' · (p' ∘ q).

Русский

Пусть p,q ∈ R[X]. Тогда производная композиции 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 (p q : R[X]) : derivative (p.comp q) = derivative q * p.derivative.comp q :=
  by
  induction p using Polynomial.induction_on'
  · simp [*, mul_add]
  · simp only [derivative_pow, derivative_mul, monomial_comp, derivative_monomial, derivative_C, zero_mul, C_eq_natCast,
      zero_add, RingHom.map_mul]
    ring

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