Commit 2022-06-02 19:38 e4433311View on Github →
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
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