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)
- depends on: #16440