hasDerivAt — Mathlib

English

The derivative of the polynomial evaluation function is p.derivative.eval x.

Русский

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

LaTeX

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

Lean4

/-- The derivative (in the analysis sense) of a polynomial `p` is given by `p.derivative`. -/
protected theorem hasDerivAt (x : 𝕜) : HasDerivAt (fun x => p.eval x) (p.derivative.eval x) x :=
  (p.hasStrictDerivAt x).hasDerivAt

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