deriv_mul — Mathlib

English

If c and d are differentiable at x, then the derivative of the product y ↦ c(y) d(y) equals the standard product rule expression.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem deriv_mul (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) :
    deriv (c * d) x = deriv c x * d x + c x * deriv d x :=
  (hc.hasDerivAt.mul hd.hasDerivAt).deriv

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