const_mul — Mathlib

English

If a is differentiable at x, then the map y ↦ c(y) d has derivative at x equal to d times the derivative of c at x.

Русский

Если c дифференцируема в точке x, то производная отображения y ↦ c(y) d в x равна d умноженному на производную c в x.

LaTeX

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

Lean4

@[fun_prop]
theorem const_mul (ha : HasFDerivAt a a' x) (b : 𝔸) : HasFDerivAt (fun y => b * a y) (b • a') x :=
  ((ContinuousLinearMap.mul 𝕜 𝔸) b).hasFDerivAt.comp x ha

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