English
If the splitting condition holds for all x, then the normal closure inside the normal closure is itself normal.
Русский
Если выполняется условие распада для всех x, то нормальное замыкание внутри нормального замыкания само является нормальным.
LaTeX
$$$\forall x:K,\;\text{Splits}(\minpoly(F,x))(L)\Rightarrow \text{IsNormalClosure }F K(\text{Subtype}...)$$
Lean4
/-- If `K/F` is algebraic, the "generated by roots" condition in IsNormalClosure can be replaced
by "generated by images of embeddings". -/
theorem isNormalClosure_iff :
IsNormalClosure F K L ↔ (∀ x : K, (minpoly F x).Splits (algebraMap F L)) ∧ normalClosure F K L = ⊤ := by
refine ⟨fun ⟨splits, h⟩ ↦ ⟨splits, ?_⟩, fun ⟨splits, h⟩ ↦ ⟨splits, ?_⟩⟩ <;>
simpa only [normalClosure_eq_iSup_adjoin_of_splits splits] using h
