mathlib

4d909f41 - feat(analysis/calculus/local_extr): A polynomial's roots are bounded by its derivative (#7571)

feat(analysis/calculus/local_extr): A polynomial's roots are bounded by its derivative (#7571) An application of Rolle's theorem to polynomials. Co-authored-by: Thomas Browning <tb65536@uw.edu>