deriv_single

Mathlib.Analysis.Calculus.Deriv.Pi

URI: https://scilib.ai/kg/mathlib#deriv_single

English

The derivative of the polynomial evaluation map is given by p.derivative evaluated at x.

Русский

Производная отображения p.eval равна p.derivative.eval x.

LaTeX

$$$HasDerivAt\$\\lambda x. p.eval x\$\\left(p.derivative.eval x\\right) x$$$

Lean4

theorem deriv_single (i : ι) (y : 𝕜) : deriv (Pi.single (M := fun _ ↦ 𝕜) i) y = Pi.single i (1 : 𝕜) :=
  deriv_update 0 i y

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

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

Разделы

Аффилиация

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