Commit 2022-11-15 22:05 fc7dbc95

View on Github →

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.

Estimated changes

Modified src/analysis/calculus/local_extr.lean

modified theorem polynomial.card_root_set_le_derivative

added theorem polynomial.card_roots_le_derivative

added theorem polynomial.card_roots_to_finset_le_card_roots_derivative_diff_roots_succ

added theorem polynomial.card_roots_to_finset_le_derivative

Modified src/data/finset/lattice.lean

added theorem finset.card_le_diff_of_interleaved

added theorem finset.card_le_of_interleaved

added theorem finset.exists_next_left

added theorem finset.exists_next_right

added theorem finset.max_mem_image_coe

added theorem finset.max_mem_insert_bot_image_coe

added theorem finset.min_mem_image_coe

added theorem finset.min_mem_insert_top_image_coe

Modified src/data/finset/sort.lean

deleted theorem finset.card_le_of_interleaved

Modified src/data/polynomial/derivative.lean

added theorem polynomial.eq_C_of_derivative_eq_zero

modified theorem polynomial.nat_degree_eq_zero_of_derivative_eq_zero