Commit 2021-01-30 20:09 a6c0442b

View on Github →

feat(field_theory/normal): Restriction is surjective (#5960) Proves surjectivity of alg_equiv.restrict_normal_hom. Also proves a bijectivity lemma which gives a cleaner construction of alg_equiv.restrict_normal.

Estimated changes

Modified src/field_theory/normal.lean

added theorem alg_equiv.lift_normal_commutes

added theorem alg_equiv.restrict_lift_normal

modified theorem alg_equiv.restrict_normal_commutes

added theorem alg_equiv.restrict_normal_hom_surjective

added theorem alg_hom.lift_normal_commutes

added theorem alg_hom.normal_bijective

added theorem alg_hom.restrict_lift_normal

modified theorem alg_hom.restrict_normal_commutes