∀ {F : Type u_1} {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K]
  [toIsAlgebraic : Algebra.IsAlgebraic F K],
  (∀ (x : K), (Polynomial.map (algebraMap F K) (minpoly F x)).Splits) → Normal F K