Theorems · Theorem · real analysis

Polynomial.hasStrictDerivAt

∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (p : Polynomial 𝕜) (x : 𝕜),
  HasStrictDerivAt (fun x => Polynomial.eval x p) (Polynomial.eval x (Polynomial.derivative p)) x

The derivative (in the analysis sense) of a polynomial p is given by p.derivative.

Defined in

Mathlib.Analysis.Calculus.Deriv.Polynomial

Cited by

3 results in Mathlib

Foundations

Depth 188 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedField