hasDerivAt_mul_const — Mathlib

English

If hc and hd are HasDerivAt for c and d, then the product rule yields the derivative of c(y) d(y) at x as 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{HasDerivAt}(c \cdot d) x = c'(x) \cdot d(x) + c(x) \cdot d'(x)$$$

Lean4

theorem hasDerivAt_mul_const (c : 𝕜) : HasDerivAt (fun x => x * c) c x := by
  simpa only [one_mul] using (hasDerivAt_id' x).mul_const c

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