smul — Mathlib

English

If c and f have strict derivatives at x with derivatives c' and f', then the product c(y) f(y) has strict derivative at x equal to c(x) f' + c' f(x).

Русский

Если c и f имеют строгие производные в x, то произведение c(y) f(y) имеет строгую производную в x, равную c(x) f'(x) + c'(x) f(x).

LaTeX

$$$\\dfrac{d}{dy}\\bigl(c(y)f(y)\\bigr)\\Big|_{y=x} = c(x)\\,f'(x) + c'(x)\\,f(x)$$$

Lean4

nonrec theorem smul (hc : HasStrictDerivAt c c' x) (hf : HasStrictDerivAt f f' x) :
    HasStrictDerivAt (c • f) (c x • f' + c' • f x) x := by simpa using (hc.smul hf).hasStrictDerivAt

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