# Documentation

Mathlib.Analysis.Calculus.LocalExtr.Polynomial

# Rolle's Theorem for polynomials #

In this file we use Rolle's Theorem to relate the number of real roots of a real polynomial and its derivative. Namely, we prove the following facts.

• Polynomial.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ: the number of roots of a real polynomial p is at most the number of roots of its derivative that are not roots of p plus one.
• Polynomial.card_roots_toFinset_le_derivative, Polynomial.card_rootSet_le_derivative: the number of roots of a real polynomial is at most the number of roots of its derivative plus one.
• Polynomial.card_roots_le_derivative: same, but the roots are counted with multiplicities.

## Keywords #

polynomial, Rolle's Theorem, root

The number of roots of a real polynomial p is at most the number of roots of its derivative that are not roots of p plus one.

The number of roots of a real polynomial is at most the number of roots of its derivative plus one.

theorem Polynomial.card_roots_le_derivative (p : ) :
Multiset.card () Multiset.card (Polynomial.roots (Polynomial.derivative p)) + 1

The number of roots of a real polynomial (counted with multiplicities) is at most the number of roots of its derivative (counted with multiplicities) plus one.

theorem Polynomial.card_rootSet_le_derivative {F : Type u_1} [] [] (p : ) :
Fintype.card ↑(Polynomial.rootSet (Polynomial.derivative p) ) + 1

The number of real roots of a polynomial is at most the number of roots of its derivative plus one.