English
Let c be differentiable at x with respect to the 𝕜-normed structure, and let d be a fixed element. Then the derivative at x of the map y ↦ c(y) d exists and equals d multiplied by the derivative of c at x; i.e., f′(x) = d · fderiv 𝕜 c x.
Русский
Пусть c дифференцируема в точке x относительно 𝕜, и фиксировано задан элемент d. Производная в точке x от отображения y ↦ c(y) d существует и равна произведению d на производную c в x; т.е. f′(x) = 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_mul_const (hc : DifferentiableAt 𝕜 c x) (d : 𝔸') : fderiv 𝕜 (fun y => c y * d) x = d • fderiv 𝕜 c x :=
(hc.hasFDerivAt.mul_const d).fderiv
