Algebraic closure is normal

Stream: Is there code for X?

[Xavier Roblot]

Is it true that these results are missing?

import field_theory.is_alg_closed.algebraic_closure
import field_theory.normal

variables {R K : Type*} [field R] [field K] [algebra R K]

lemma is_alg_closure.normal (h : is_alg_closure R K) : normal R K :=
⟨h.algebraic, λ _, @is_alg_closed.splits_codomain _ _ _ h.alg_closed _ _ _⟩

instance : normal K (algebraic_closure K) :=
  is_alg_closure.normal (algebraic_closure.is_alg_closure _)

[Ruben Van de Velde]

is_alg_closed only seems used in three files under src/field_theory/is_alg_closed/, so if it's not there, it's not in mathlib

[Xavier Roblot]

#18730