# 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 : Polynomial ℝ)
:

Finset.card (Multiset.toFinset (Polynomial.roots p)) ≤ Finset.card
(Multiset.toFinset (Polynomial.roots (↑Polynomial.derivative p)) \ Multiset.toFinset (Polynomial.roots p)) + 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 : Polynomial ℝ)
:

Finset.card (Multiset.toFinset (Polynomial.roots p)) ≤ Finset.card (Multiset.toFinset (Polynomial.roots (↑Polynomial.derivative p))) + 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 : Polynomial ℝ)
:

↑Multiset.card (Polynomial.roots p) ≤ ↑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}
[CommRing F]
[Algebra F ℝ]
(p : Polynomial F)
:

Fintype.card ↑(Polynomial.rootSet 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.