deriv_mul_const_field' — Mathlib

English

If c and d are differentiable at x, then the derivative of the product (as a function) is given by the sum of two products: c'(x) d(x) + c(x) d'(x).

Русский

Если c и d дифференцируемы в 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

@[simp]
theorem deriv_mul_const_field' (v : 𝕜') : (deriv fun x => u x * v) = fun x => deriv u x * v :=
  funext fun _ => deriv_mul_const_field v

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