smul — Mathlib

English

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

Русский

Если c и f дифференцируемы в точке x с производными c'(x) и f'(x), тогда производная в x функции y ↦ c(y) f(y) равна 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 smul (hc : HasDerivAt c c' x) (hf : HasDerivAt f f' x) : HasDerivAt (c • f) (c x • f' + c' • f x) x :=
  hc.fun_smul hf

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