mathlib

fc7dbc95 - feat(analysis/calculus/local_extr): generalize `polynomial.card_root_set_le_derivative` (#17315)

feat(analysis/calculus/local_extr): generalize `polynomial.card_root_set_le_derivative` (#17315) Generalize from `field` to `comm_ring`. Also add a version about the number of roots counted with multiplicities.