Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-16 13:18 4d909f41

View on Github →

feat(analysis/calculus/local_extr): A polynomial's roots are bounded by its derivative (#7571) An application of Rolle's theorem to polynomials.

Estimated changes

Modified src/algebra/char_zero.lean

added theorem ring_hom.char_zero

added theorem ring_hom.char_zero_iff

Modified src/analysis/calculus/local_extr.lean

added theorem polynomial.card_root_set_le_derivative

Modified src/data/finset/sort.lean

added theorem finset.card_le_of_interleaved