feat(field_theory/is_alg_closed/algebraic_closure): add instances no…

…rmal and is_galois for algebraic closure (#18730)

src/field_theory/galois.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning, Patrick Lutz
 -/
 
-import field_theory.normal
+import field_theory.is_alg_closed.algebraic_closure
 import field_theory.primitive_element
 import field_theory.fixed
 import group_theory.group_action.fixing_subgroup
@@ -424,3 +424,11 @@ end
 end is_galois
 
 end galois_equivalent_definitions
+
+section is_alg_closure
+
+@[priority 100]
+instance is_alg_closure.is_galois (k K : Type*) [field k] [field K] [algebra k K]
+  [is_alg_closure k K] [char_zero k] : is_galois k K := { }
+
+end is_alg_closure

src/field_theory/is_alg_closed/algebraic_closure.lean

@@ -5,7 +5,7 @@ Authors: Kenny Lau
 -/
 import algebra.direct_limit
 import field_theory.is_alg_closed.basic
-import field_theory.splitting_field
+
 /-!
 # Algebraic Closure
 

src/field_theory/is_alg_closed/basic.lean

@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
 
+import field_theory.normal
 import field_theory.perfect_closure
-import field_theory.separable
-import ring_theory.adjoin.field
 import ring_theory.localization.integral
 
 /-!
@@ -170,6 +169,19 @@ theorem is_alg_closure_iff (K : Type v) [field K] [algebra k K] :
   is_alg_closure k K ↔ is_alg_closed K ∧ algebra.is_algebraic k K :=
 ⟨λ h, ⟨h.1, h.2⟩, λ h, ⟨h.1, h.2⟩⟩
 
+@[priority 100]
+instance is_alg_closure.normal (R K : Type*) [field R] [field K] [algebra R K] [is_alg_closure R K]:
+  normal R K :=
+⟨is_alg_closure.algebraic, λ _,
+  @is_alg_closed.splits_codomain _ _ _ (is_alg_closure.alg_closed R) _ _ _⟩
+
+@[priority 100]
+instance is_alg_closure.separable (R K : Type*) [field R] [field K] [algebra R K]
+[is_alg_closure R K] [char_zero R] :
+  is_separable R K :=
+⟨λ _, is_algebraic_iff_is_integral.mp (is_alg_closure.algebraic _), λ _, (minpoly.irreducible
+  (is_algebraic_iff_is_integral.mp (is_alg_closure.algebraic _))).separable⟩
+
 namespace lift
 
 /- In this section, the homomorphism from any algebraic extension into an algebraically