English
If every minpoly x splits in L, then the normal closure equals the iSup over x∈K of adjoin F rootSet of minpoly x in L.
Русский
Если каждый minpoly x распадается в L, то нормальное замыкание равно iSup по x∈K от adjoin F корневого множества minpoly x в L.
LaTeX
$$$(\forall x:K,\minpoly F x).Splits (algebraMap F L)\Rightarrow \operatorname{normalClosure} F K L = \big\langle x:K, adjoin F ((\minpoly F x).rootSet L)\big\rangle$$$
Lean4
theorem normalClosure_le_iSup_adjoin :
normalClosure F K L ≤ ⨆ x : K, IntermediateField.adjoin F ((minpoly F x).rootSet L) :=
iSup_le fun f _ ⟨x, hx⟩ ↦
le_iSup (α := IntermediateField F L) _ x <|
IntermediateField.subset_adjoin F _ <| by
rw [mem_rootSet_of_ne (minpoly.ne_zero (Algebra.IsIntegral.isIntegral x)), ← hx, AlgHom.toRingHom_eq_coe,
AlgHom.coe_toRingHom, aeval_algHom_apply, minpoly.aeval, map_zero]
