Commit 2022-09-22 06:54 f4210e94

View on Github →

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)

Estimated changes