deriv_const_mul_field' — Mathlib

English

Derivative within s of a constant multiple equals the constant times derivative within s of the original function.

Русский

Производная внутри s от константного множителя равна константе, умноженной на производную внутри s от исходной функции.

LaTeX

$$$ \mathrm{derivWithin}_s (u \cdot v)(x) = u \cdot \mathrm{derivWithin}_s v(x) $$$

Lean4

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

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