deriv_smul — Mathlib

English

If c and f are differentiable at x, then the derivative of y ↦ c(y) f(y) at x is c(x) f'(x) + c'(x) f(x).

Русский

Если c и f дифференцируемы в точке x, то производная y ↦ c(y) f(y) в x равна c(x) f'(x) + c'(x) f(x).

LaTeX

$$$\\dfrac{d}{dy}\\bigl(c(y)f(y)\\bigr)\\Big|_{y=x} = c(x)\\,f'(x) + c'(x)\\,f(x)$$$

Lean4

theorem deriv_smul (hc : DifferentiableAt 𝕜 c x) (hf : DifferentiableAt 𝕜 f x) :
    deriv (c • f) x = c x • deriv f x + deriv c x • f x :=
  (hc.hasDerivAt.smul hf.hasDerivAt).deriv

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