hasDerivAt_aeval — Mathlib

English

Let 𝕜 be a nontrivially normed field, R a commutative semiring with an algebra structure R → 𝕜, and q ∈ R[X]. Then the map x ↦ aeval x q is differentiable at x with derivative aeval x (derivative q).

Русский

Пусть 𝕜 — ненулевое нормированное поле, R — коммутативное полное кольцо с отображением алгебра R → 𝕜, и q ∈ R[X]. Тогда отображение x ↦ aeval x q дифференцируемо в точке x и его производная равна aeval x (derivative q).

LaTeX

$$$HasDerivAt\left(\lambda x, aeval\, x\ q\right)\left( aeval\, x\,(derivative\ q) \right) x$$$

Lean4

protected theorem hasDerivAt_aeval (x : 𝕜) : HasDerivAt (fun x => aeval x q) (aeval x (derivative q)) x :=
  (q.hasStrictDerivAt_aeval x).hasDerivAt

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