Commit 2021-01-29 19:10 e8e05265

View on Github →

feat(field_theory/polynomial_galois_group): New file (#5861) This PR adds the file polynomial_galois_group. It contains some of the groundwork needed for proving the Abel-Ruffini theorem.

Estimated changes

Modified src/data/polynomial/field_division.lean

added theorem polynomial.mem_root_set

Modified src/data/polynomial/ring_division.lean

added def polynomial.root_set

added theorem polynomial.root_set_def

added theorem polynomial.root_set_zero

Modified src/field_theory/normal.lean

modified theorem normal.of_is_splitting_field

Created src/field_theory/polynomial_galois_group.lean

added theorem polynomial.gal.card_of_separable

added def polynomial.gal.gal_action_hom

added theorem polynomial.gal.gal_action_hom_injective

added def polynomial.gal.map_roots

added theorem polynomial.gal.map_roots_bijective

added theorem polynomial.gal.prime_degree_dvd_card

added def polynomial.gal.restrict

added def polynomial.gal.restrict_dvd

added def polynomial.gal.restrict_prod

added theorem polynomial.gal.restrict_prod_injective

added theorem polynomial.gal.restrict_smul

added def polynomial.gal.roots_equiv_roots

added def polynomial.gal

Modified src/field_theory/splitting_field.lean

added theorem polynomial.splitting_field.adjoin_root_set