mathlib

e4433311 - refactor(field_theory/normal): generalize `lift_normal` and `restrict_normal` (#14450)

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