noncomputable def FieldExtensionsGalois.algebraicClosureInL (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] : IntermediateField K L

theorem FieldExtensionsGalois.isSeparable_iff_minpoly_separable (F : Type u_1) (E : Type u_2) [Field F] [Field E] [Algebra F E] [Algebra.IsAlgebraic F E] : Algebra.IsSeparable F E ↔ ∀ (α : E), (minpoly F α).Separable