mathlib3

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

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).