mathlib3

6e59fbe3 - feat(field_theory/splitting_field): generalize some results from field to domain (#10726)

feat(field_theory/splitting_field): generalize some results from field to domain (#10726) This PR does a few things generalizing / golfing facts related to polynomials and splitting fields. - Generalize some results in `data.polynomial.field_division` to division rings - generalize `C_leading_coeff_mul_prod_multiset_X_sub_C` from a field to a domain - same for `prod_multiset_X_sub_C_of_monic_of_roots_card_eq` - add a supporting useful lemma `roots_map_of_injective_card_eq_total_degree` saying that if we already have a full (multi)set of roots over a domain, passing along an injection gives the set of roots of the mapped polynomial Inspired by needs of flt-regular. Co-authored-by: Johan Commelin <johan@commelin.net>