deriv_const_mul_field — Mathlib

English

If u is a constant and v is a function, then the derivative of y ↦ u · v(y) is u times the derivative of v.

Русский

Если u — константа, а v — функция, то производная от y ↦ u · v(y) равна u · v'(y).

LaTeX

$$$ \frac{d}{dx} \bigl( u \cdot v(x) \bigr) = u \cdot v'(x) $$$

Lean4

theorem deriv_const_mul_field (u : 𝕜') : deriv (fun y => u * v y) x = u * deriv v x := by
  simp only [mul_comm u, deriv_mul_const_field]

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