Commit 2022-06-02 19:38 e4433311

View on Github →

refactor(field_theory/normal): generalize lift_normal and restrict_normal (#14450) This generalization seems useful. The example I have in mind is restricting a map ϕ : E →ₐ[F] (algebraic_closure E) to a map ϕ : E →ₐ[F] E when E/F is normal. Coauthored by @mariainesdff

Estimated changes

Modified src/field_theory/normal.lean

modified theorem alg_equiv.lift_normal_commutes

modified theorem alg_equiv.restrict_lift_normal

modified def alg_equiv.restrict_normal_hom

modified theorem alg_equiv.restrict_normal_hom_surjective

modified theorem alg_hom.lift_normal_commutes

modified theorem alg_hom.restrict_lift_normal

added def alg_hom.restrict_normal'

modified theorem is_solvable_of_is_scalar_tower