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_sdiff_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_sdiff_roots_succ (p : Polynomial ℝ) : p.roots.toFinset.card ≤ ((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.

@[deprecated Polynomial.card_roots_toFinset_le_card_roots_derivative_sdiff_roots_succ (since := "2026-06-03")]

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

Alias of Polynomial.card_roots_toFinset_le_card_roots_derivative_sdiff_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.

theorem Polynomial.card_roots_toFinset_le_derivative (p : Polynomial ℝ) : p.roots.toFinset.card ≤ (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 ℝ) : p.roots.card ≤ (derivative p).roots.card + 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 ↑((derivative p).rootSet ℝ) + 1

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