Commit 2021-12-18 18:09 6e59fbe3

View on Github →

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.

Estimated changes

Modified src/data/multiset/basic.lean

added theorem multiset.count_map

added theorem multiset.count_map_eq_count'

Modified src/data/polynomial/field_division.lean

modified theorem polynomial.prod_multiset_root_eq_finset_root

modified theorem polynomial.roots_C_mul

modified theorem polynomial.roots_normalize

Modified src/data/polynomial/ring_division.lean

added theorem polynomial.count_map_roots

added theorem polynomial.le_root_multiplicity_map

added theorem polynomial.roots_map_of_injective_card_eq_total_degree

Modified src/field_theory/splitting_field.lean

modified theorem polynomial.C_leading_coeff_mul_prod_multiset_X_sub_C

added theorem polynomial.C_leading_coeff_mul_prod_multiset_X_sub_C_of_field

modified theorem polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq

added theorem polynomial.prod_multiset_X_sub_C_of_monic_of_roots_card_eq_of_field