const_mul — Mathlib

English

If c and d are differentiable at x, then the derivative of the product c(y) d(y) at x is c'(x) d(x) + c(x) d'(x).

Русский

Если c и d дифференцируемы в x, то производная от произведения c(y) d(y) в x равна c'(x) d(x) + c(x) d'(x).

LaTeX

$$$\operatorname{deriv}(y \mapsto c(y) d(y)) x = c'(x) d(x) + c(x) d'(x)$$$

Lean4

theorem const_mul (c : 𝔸) (hd : HasDerivWithinAt d d' s x) : HasDerivWithinAt (fun y => c * d y) (c * d') s x :=
  by
  convert (hasDerivWithinAt_const x s c).mul hd using 1
  rw [zero_mul, zero_add]

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