# mathlib3documentation

analysis.calculus.deriv.polynomial

# Derivatives of polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove that derivatives of polynomials in the analysis sense agree with their derivatives in the algebraic sense.

For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of analysis/calculus/deriv/basic.

## TODO #

• Generalize some (most?) results to an algebra over the base field.

## Keywords #

derivative, polynomial

### Derivative of a polynomial #

@[protected]
theorem polynomial.has_strict_deriv_at {𝕜 : Type u} (p : polynomial 𝕜) (x : 𝕜) :
has_strict_deriv_at (λ (x : 𝕜), p) x

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

@[protected]
theorem polynomial.has_strict_deriv_at_aeval {𝕜 : Type u} {R : Type u_1} [ 𝕜] (q : polynomial R) (x : 𝕜) :
has_strict_deriv_at (λ (x : 𝕜), q) ( x
@[protected]
theorem polynomial.has_deriv_at {𝕜 : Type u} (p : polynomial 𝕜) (x : 𝕜) :
has_deriv_at (λ (x : 𝕜), p) x

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

@[protected]
theorem polynomial.has_deriv_at_aeval {𝕜 : Type u} {R : Type u_1} [ 𝕜] (q : polynomial R) (x : 𝕜) :
has_deriv_at (λ (x : 𝕜), q) ( x
@[protected]
theorem polynomial.has_deriv_within_at {𝕜 : Type u} (p : polynomial 𝕜) (x : 𝕜) (s : set 𝕜) :
has_deriv_within_at (λ (x : 𝕜), p) s x
@[protected]
theorem polynomial.has_deriv_within_at_aeval {𝕜 : Type u} {R : Type u_1} [ 𝕜] (q : polynomial R) (x : 𝕜) (s : set 𝕜) :
has_deriv_within_at (λ (x : 𝕜), q) ( s x
@[protected]
theorem polynomial.differentiable_at {𝕜 : Type u} {x : 𝕜} (p : polynomial 𝕜) :
(λ (x : 𝕜), p) x
@[protected]
theorem polynomial.differentiable_at_aeval {𝕜 : Type u} {x : 𝕜} {R : Type u_1} [ 𝕜] (q : polynomial R) :
(λ (x : 𝕜), q) x
@[protected]
theorem polynomial.differentiable_within_at {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} (p : polynomial 𝕜) :
(λ (x : 𝕜), p) s x
@[protected]
theorem polynomial.differentiable_within_at_aeval {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {R : Type u_1} [ 𝕜] (q : polynomial R) :
(λ (x : 𝕜), q) s x
@[protected]
theorem polynomial.differentiable {𝕜 : Type u} (p : polynomial 𝕜) :
(λ (x : 𝕜), p)
@[protected]
theorem polynomial.differentiable_aeval {𝕜 : Type u} {R : Type u_1} [ 𝕜] (q : polynomial R) :
(λ (x : 𝕜), q)
@[protected]
theorem polynomial.differentiable_on {𝕜 : Type u} {s : set 𝕜} (p : polynomial 𝕜) :
(λ (x : 𝕜), p) s
@[protected]
theorem polynomial.differentiable_on_aeval {𝕜 : Type u} {s : set 𝕜} {R : Type u_1} [ 𝕜] (q : polynomial R) :
(λ (x : 𝕜), q) s
@[protected, simp]
theorem polynomial.deriv {𝕜 : Type u} {x : 𝕜} (p : polynomial 𝕜) :
deriv (λ (x : 𝕜), p) x =
@[protected, simp]
theorem polynomial.deriv_aeval {𝕜 : Type u} {x : 𝕜} {R : Type u_1} [ 𝕜] (q : polynomial R) :
deriv (λ (x : 𝕜), q) x =
@[protected]
theorem polynomial.deriv_within {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} (p : polynomial 𝕜) (hxs : x) :
deriv_within (λ (x : 𝕜), p) s x =
@[protected]
theorem polynomial.deriv_within_aeval {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {R : Type u_1} [ 𝕜] (q : polynomial R) (hxs : x) :
deriv_within (λ (x : 𝕜), q) s x =
@[protected]
theorem polynomial.has_fderiv_at {𝕜 : Type u} (p : polynomial 𝕜) (x : 𝕜) :
has_fderiv_at (λ (x : 𝕜), p) (1.smul_right x
@[protected]
theorem polynomial.has_fderiv_at_aeval {𝕜 : Type u} {R : Type u_1} [ 𝕜] (q : polynomial R) (x : 𝕜) :
has_fderiv_at (λ (x : 𝕜), q) (1.smul_right ( x
@[protected]
theorem polynomial.has_fderiv_within_at {𝕜 : Type u} {s : set 𝕜} (p : polynomial 𝕜) (x : 𝕜) :
has_fderiv_within_at (λ (x : 𝕜), p) (1.smul_right s x
@[protected]
theorem polynomial.has_fderiv_within_at_aeval {𝕜 : Type u} {s : set 𝕜} {R : Type u_1} [ 𝕜] (q : polynomial R) (x : 𝕜) :
has_fderiv_within_at (λ (x : 𝕜), q) (1.smul_right ( s x
@[protected, simp]
theorem polynomial.fderiv {𝕜 : Type u} {x : 𝕜} (p : polynomial 𝕜) :
(λ (x : 𝕜), p) x =
@[protected, simp]
theorem polynomial.fderiv_aeval {𝕜 : Type u} {x : 𝕜} {R : Type u_1} [ 𝕜] (q : polynomial R) :
(λ (x : 𝕜), q) x = 1.smul_right (
@[protected]
theorem polynomial.fderiv_within {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} (p : polynomial 𝕜) (hxs : x) :
(λ (x : 𝕜), p) s x =
@[protected]
theorem polynomial.fderiv_within_aeval {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {R : Type u_1} [ 𝕜] (q : polynomial R) (hxs : x) :
(λ (x : 𝕜), q) s x = 1.smul_right (