deriv_smul_const — 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 product y ↦ c f(y) has derivative c f'(x).

Русский

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

LaTeX

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

Lean4

theorem deriv_smul_const (hc : DifferentiableAt 𝕜 c x) (f : F) : deriv (fun y => c y • f) x = deriv c x • f :=
  (hc.hasDerivAt.smul_const f).deriv

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