derivWithin_aeval — Mathlib

English

For q ∈ Polynomial R, the derivative of the map x ↦ aeval x q at x equals aeval x (derivative q).

Русский

Для q ∈ Polynomial R производная отображения x ↦ aeval x q в точке x равна aeval x (derivative q).

LaTeX

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

Lean4

protected theorem derivWithin_aeval (hxs : UniqueDiffWithinAt 𝕜 s x) :
    derivWithin (fun x => aeval x q) s x = aeval x (derivative q) := by
  simpa only [aeval_def, eval₂_eq_eval_map, derivative_map] using (q.map (algebraMap R 𝕜)).derivWithin hxs

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