English
If c has a strict derivative c' at x and f has a strict derivative f' at x, then the map y ↦ c(y)·f(y) has the derivative c(x)·f' + c' smulRight (f x) at x.
Русский
Если c имеет строгую производную c' в точке x и f имеет строгую производную f' в x, то функция y ↦ c(y)·f(y) имеет производную в x равную c(x)·f' + c' smulRight (f(x)).
LaTeX
$$$$ \\text{HasStrictFDerivAt}(\\lambda y, c(y)\\,\\cdot\\, f(y), x) = c(x)·f' + c'\\smulRight(f(x)). $$$$
Lean4
@[fun_prop]
theorem fun_smul (hc : HasStrictFDerivAt c c' x) (hf : HasStrictFDerivAt f f' x) :
HasStrictFDerivAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) x :=
(isBoundedBilinearMap_smul.hasStrictFDerivAt (c x, f x)).comp x <| hc.prodMk hf
