English
If every monic irreducible polynomial over F has a root in E, then E is an algebraic closure of F.
Русский
Если каждый монический неприводимый многочлен над F имеет корень в E, то E является алгебраическим замыканием F.
LaTeX
$$$\\Bigl(\\forall p\\in F[X],\\ p\\text{ моничный} \\land \\text{ неприводимый } p \\Rightarrow \\exists x\\in E, aeval(x)p=0\\Bigr) \\Rightarrow IsAlgClosure\\ F\\ E$$
Lean4
theorem _root_.IsAlgClosure.of_exist_roots (h : ∀ p : F[X], p.Monic → Irreducible p → ∃ x : E, aeval x p = 0) :
IsAlgClosure F E :=
.of_splits fun p _ _ ↦
have ⟨σ⟩ :=
nonempty_algHom_of_exist_roots fun x : p.SplittingField ↦
have := Algebra.IsAlgebraic.isIntegral (K := F).1 x
h _ (minpoly.monic this) (minpoly.irreducible this)
splits_of_algHom (SplittingField.splits _) σ
