Commit 2021-02-11 16:20 f151da2a

View on Github →

feat(field_theory/polynomial_galois_group): Restriction from splitting field of composition (#6148) Defines the surjective restriction map from the splitting field of a composition

Estimated changes

Modified src/field_theory/polynomial_galois_group.lean

added theorem polynomial.gal.mul_splits_in_splitting_field_of_mul

added def polynomial.gal.restrict_comp

added theorem polynomial.gal.restrict_comp_surjective

added theorem polynomial.gal.splits_in_splitting_field_of_comp