deriv

Mathlib.Analysis.Calculus.Deriv.Polynomial

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

English

For p ∈ 𝕜[X], the map x ↦ p.eval x is differentiable on the whole domain 𝕜.

Русский

Для p ∈ 𝕜[X] функция x ↦ p.eval x дифференцируема на всём 𝕜.

LaTeX

$$$Differentiable\ _{\mathbb{K}}$\lambda x, p.eval x$$$$

Lean4

@[simp]
protected theorem deriv : deriv (fun x => p.eval x) x = p.derivative.eval x :=
  (p.hasDerivAt x).deriv

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

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

Разделы

Аффилиация

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