Theorem Polynomial.rootSet_derivative_subset_convexHull_rootSet

Modification history

2025-10-01 21:33
Mathlib/Analysis/Complex/Polynomial/GaussLucas.lean
feat: prove Gauss-Lucas theorem (#29630) …
Added Polynomial.rootSet_derivative_subset_convexHull_rootSetView on Github →