Commit 2025-10-01 21:33 9699f52a

View on Github →

feat: prove Gauss-Lucas theorem (#29630) The proof was found by Aristotle AI, then rewritten by me in Mathlib style.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Polynomial/Eval/Defs.lean

added theorem Polynomial.eval_listSum

modified theorem Polynomial.eval_mul_X

added theorem Polynomial.eval_multisetSum

Modified Mathlib/Algebra/Polynomial/Splits.lean

added theorem Polynomial.aeval_derivative_of_splits

added theorem Polynomial.eval_derivative_div_eval_of_ne_zero_of_splits

added theorem Polynomial.eval_derivative_eq_eval_mul_sum_of_splits

added theorem Polynomial.eval_derivative_of_splits

added theorem Polynomial.eval₂_derivative_of_splits

Created Mathlib/Analysis/Complex/Polynomial/GaussLucas.lean

added theorem Polynomial.derivRootWeight_nonneg

added theorem Polynomial.eq_centerMass_of_eval_derivative_eq_zero

added theorem Polynomial.rootSet_derivative_subset_convexHull_rootSet

added theorem Polynomial.sum_derivRootWeight_pos

Modified docs/1000.yaml