# 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

theorem Polynomial.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ (p : ) :
p.roots.toFinset.card ((Polynomial.derivative p).roots.toFinset \ p.roots.toFinset).card + 1

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.

theorem Polynomial.card_roots_toFinset_le_derivative (p : ) :
p.roots.toFinset.card (Polynomial.derivative p).roots.toFinset.card + 1

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 p.roots Multiset.card (Polynomial.derivative p).roots + 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 (p.rootSet ) Fintype.card ((Polynomial.derivative p).rootSet ) + 1

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