Commit 2025-09-26 08:53 7ba3757f

feat(FieldTheory/IsGalois): map induced by the restriction to a subfield (#26841) For E/L a field extension and K a subfield of E, we define the map (E ≃ₐ[L] E) →* (K ≃ₐ[F] K) induced by the restriction to K (with F a subfield of K and L such that K/F is normal) and study when it is injective and surjective.