const_smul — Mathlib

English

If c is a constant from a ring R acting on F and f is differentiable at x with derivative f', then the derivative of y ↦ c • f(y) at x is c • f'.

Русский

Если константа c из кольца R действует на F и f дифференцируема в x c производной f', тогда производная y ↦ c • f(y) в x равна c • f'(x).

LaTeX

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

Lean4

nonrec theorem const_smul (c : R) (hf : HasDerivAt f f' x) : HasDerivAt (c • f) (c • f') x :=
  hf.const_smul c

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