smul — Mathlib

English

The product rule for the bilinear multiplication map holds: the derivative of y ↦ c(y)·f(y) is c(x)·f' + c' smulRight (f x).

Русский

Правило произведения для билинейного умножения: производная y ↦ c(y)·f(y) равна c(x)·f' + c' smulRight (f(x)).

LaTeX

$$$$ \\text{HasStrictFDerivAt}(\\lambda y, c(y)·f(y), x) = c(x)·f' + c'.smulRight(f(x)). $$$$

Lean4

@[fun_prop]
theorem smul (hc : HasStrictFDerivAt c c' x) (hf : HasStrictFDerivAt f f' x) :
    HasStrictFDerivAt (c • f) (c x • f' + c'.smulRight (f x)) x :=
  (isBoundedBilinearMap_smul.hasStrictFDerivAt (c x, f x)).comp x <| hc.prodMk hf

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