Mathlib v3 is deprecated. Go to Mathlib v4

Theorem polynomial.card_root_set_le_derivative

Modification history

2022-11-15 22:05
src/analysis/calculus/local_extr.lean
feat(analysis/calculus/local_extr): generalize `polynomial.card_root_set_le_derivative` (#17315) …
Modified polynomial.card_root_set_le_derivativeView on Github →
2022-02-08 12:43
src/analysis/calculus/local_extr.lean
feat(*): localized `R[X]` notation for `polynomial R` (#11895) …
Modified polynomial.card_root_set_le_derivativeView on Github →
2021-05-16 13:18
src/analysis/calculus/local_extr.lean
feat(analysis/calculus/local_extr): A polynomial's roots are bounded by its derivative (#7571) …
Added polynomial.card_root_set_le_derivativeView on Github →