deriv_aeval — Mathlib

English

For any q ∈ Polynomial R and hxs, the derivative within s of x ↦ aeval x q is aeval x (derivative q).

Русский

Для q ∈ Polynomial R и hxs предельная производная внутри s от x ↦ aeval x q равна aeval x (derivative q).

LaTeX

$$$fderivWithin\_\{\mathbb{K}\}\left(\lambda x, aeval x q\right) s x = aeval x (derivative q)$$$

Lean4

@[simp]
protected theorem deriv_aeval : deriv (fun x => aeval x q) x = aeval x (derivative q) :=
  (q.hasDerivAt_aeval x).deriv

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