differentiableAt_aeval

Mathlib.Analysis.Calculus.Deriv.Polynomial

URI: https://scilib.ai/kg/mathlib#Polynomial.differentiableAt_aeval

English

For any q ∈ R[X], the map x ↦ aeval x q is differentiable at x.

Русский

Пусть q ∈ R[X]. Отображение x ↦ aeval x q дифференцируемо в точке x.

LaTeX

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

Lean4

protected theorem differentiableAt_aeval : DifferentiableAt 𝕜 (fun x => aeval x q) x :=
  (q.hasDerivAt_aeval x).differentiableAt

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru