mul — Mathlib

English

If hc and hd are HasDerivAt for c and d, then the derivative of the product c(y) d(y) is given by the standard product rule expression.

Русский

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

LaTeX

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

Lean4

theorem mul (hc : HasDerivAt c c' x) (hd : HasDerivAt d d' x) : HasDerivAt (c * d) (c' * d x + c x * d') x :=
  hc.fun_mul hd

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