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