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.

Keywords #

polynomial, Rolle's Theorem, root

theorem Polynomial.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ (p : Polynomial ) :
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 : Polynomial ) :
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 : Polynomial ) :
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} [CommRing F] [Algebra F ] (p : Polynomial F) :
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.