Commit 2022-06-24 15:26 475cf379

refactor(data/polynomial): extract/add lemmas and golf (#14888)

• Extract lemmas roots_multiset_prod_X_sub_C, nat_degree_multiset_prod_X_sub_C_eq_card, monic_prod_multiset_X_sub_C from the proof of C_leading_coeff_mul_prod_multiset_X_sub_C in ring_division.lean.
• Add the lemma exists_prod_multiset_X_sub_C_mul in ring_division.lean and roots_ne_zero_of_splits in splitting_field.lean and use them to golf nat_degree_eq_card_roots The proof of the latter originally depends on eq_prod_roots_of_splits, but now the dependency reversed, with nat_degree_eq_card_roots now used to golf eq_prod_roots_of_splits (and roots_map as well).
• Move prod_multiset_root_eq_finset_root and prod_multiset_X_sub_C_dvd from field_division.lean to ring_division.lean and golf the proof of the latter, generalizing field to is_domain.
• Remove redundant imports and the lemma exists_multiset_of_splits, because it is just one direction of splits_iff_exists_multiset, and it follows trivially from eq_prod_roots_of_splits. It couldn't be removed before this PR because roots_map and eq_prod_roots_of_splits depended on it.
• Golf splits_of_exists_multiset (independent of other changes).