smul_const — Mathlib

English

If c and f are differentiable at x with derivatives c'(x) and f'(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 smul_const (hc : HasStrictDerivAt c c' x) (f : F) : HasStrictDerivAt (fun y => c y • f) (c' • f) x :=
  by
  have := hc.smul (hasStrictDerivAt_const x f)
  rwa [smul_zero, zero_add] at this

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