fderiv_const_mul — Mathlib

English

If a is differentiable at x, then fderiv of λy. c(y) d equals d times fderiv of c at x.

Русский

Если a дифференцируема в x, то производная fderiv от λy. c(y) d равна d умножить на fderiv c в x.

LaTeX

$$$\\operatorname{fderiv}_{\\mathbb{K}}\\big(\\lambda y. c(y) \\cdot d\\big)(x) = d \\cdot \\operatorname{fderiv}_{\\mathbb{K}}(c)(x)$$$

Lean4

theorem fderiv_const_mul (ha : DifferentiableAt 𝕜 a x) (b : 𝔸) : fderiv 𝕜 (fun y => b * a y) x = b • fderiv 𝕜 a x :=
  (ha.hasFDerivAt.const_mul b).fderiv

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