differentiable

Mathlib.Analysis.Calculus.Deriv.Polynomial

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

English

For a polynomial q ∈ R[X], the map x ↦ aeval x q is differentiable (as a function of x).

Русский

Пусть q ∈ R[X]. Производная по x от x ↦ aeval x q существует.

LaTeX

$$$Differentiable\ \mathbb{K}$\lambda x, aeval x q$$$$

Lean4

@[fun_prop]
protected theorem differentiable : Differentiable 𝕜 fun x => p.eval x := fun _ => p.differentiableAt

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

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

Разделы

Аффилиация

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