English
For a polynomial p over a field F with an ℝ-algebra structure, the number of real roots of p is at most the number of real roots of its derivative plus one.
Русский
Для многочлена p над полем F с структурой алгебры над ℝ, число действительных корней p не превосходит число действительных корней производной p плюс один.
LaTeX
$$$Fintype.card \,(p.rootSet\_\mathbb{R}) \le Fintype.card \,(p.derivative.rootSet\_\mathbb{R}) + 1$$$
Lean4
/-- The number of real roots of a polynomial is at most the number of roots of its derivative plus
one. -/
theorem card_rootSet_le_derivative {F : Type*} [CommRing F] [Algebra F ℝ] (p : F[X]) :
Fintype.card (p.rootSet ℝ) ≤ Fintype.card (p.derivative.rootSet ℝ) + 1 := by
simpa only [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe, derivative_map] using
card_roots_toFinset_le_derivative (p.map (algebraMap F ℝ))
