mathlib

f4210e94 - feat(data/polynomial/ring_division): move lemmas, add lemmas (#16432)

feat(data/polynomial/ring_division): move lemmas, add lemmas (#16432) Rename `count_map_roots` to `count_map_roots_of_injective`. Add 8 lemmas: ``` le_root_multiplicity_iff root_multiplicity_le_iff pow_root_multiplicity_not_dvd _root_.multiset.prod_X_sub_C_dvd_iff_le_roots count_map_roots map_roots_le map_roots_le_of_injective card_roots_le_map ``` Remove `root_multiplicity_of_dvd`, it's just the left direction of `le_root_multiplicity_iff`. Move and golf 3 lemmas: ``` le_root_multiplicity_map (8 -> 5) eq_root_multiplicity_map (10 -> 7) roots_map_of_injective_card_eq_total_degree (7 -> 4) ``` - [x] depends on: #16440 Co-authored-by: alreadydone <junyanxumath@gmail.com> Co-authored-by: Junyan Xu <junyanxumath@gmail.com>