Commit 2021-01-27 08:41 e95928c0

View on Github →

feat(field_theory/normal): Restrict to normal subfield (#5845) Now that we know that splitting fields are normal, it makes sense to move the results of #5562 to normal.lean.

Estimated changes

Modified src/field_theory/normal.lean

added def alg_equiv.restrict_normal

added theorem alg_equiv.restrict_normal_commutes

added def alg_equiv.restrict_normal_hom

added theorem alg_equiv.restrict_normal_trans

added def alg_hom.restrict_normal

added def alg_hom.restrict_normal_aux

added theorem alg_hom.restrict_normal_commutes

added theorem alg_hom.restrict_normal_comp

Modified src/field_theory/splitting_field.lean

deleted def alg_equiv.restict_is_splitting_field_hom

deleted def alg_equiv.restrict_is_splitting_field

deleted theorem alg_equiv.restrict_is_splitting_field_commutes

deleted theorem alg_equiv.restrict_is_splitting_field_trans

deleted def alg_hom.restrict_is_splitting_field

deleted def alg_hom.restrict_is_splitting_field_aux

deleted theorem alg_hom.restrict_is_splitting_field_commutes

deleted theorem alg_hom.restrict_is_splitting_field_comp

deleted theorem is_splitting_field.range_to_alg_hom