English
If every nonconstant polynomial over a field k is split in an algebraically closed extension K, then k is algebraically closed.
Русский
Если каждый противолинейный ненулевой многочлен над полем k раскладывается в алгебраически замкнутом расширении K, то k алгебраически замкнуто.
LaTeX
$$$(\forall p : k[X], p.Monic \rightarrow Irreducible p \rightarrow p.Splits (\mathrm{algebraMap}\; k\; K)) \rightarrow IsAlgClosure k K$$$
Lean4
/-- If every nonconstant polynomial over `k` has a root, then `k` is algebraically closed.
-/
@[stacks 09GR "(3) ⟹ (4)"]
theorem of_exists_root (H : ∀ p : k[X], p.Monic → Irreducible p → ∃ x, p.eval x = 0) : IsAlgClosed k :=
by
refine ⟨fun p ↦ Or.inr ?_⟩
intro q hq _
have : Irreducible (q * C (leadingCoeff q)⁻¹) := by
classical
rw [← coe_normUnit_of_ne_zero hq.ne_zero]
exact (associated_normalize _).irreducible hq
obtain ⟨x, hx⟩ := H (q * C (leadingCoeff q)⁻¹) (monic_mul_leadingCoeff_inv hq.ne_zero) this
exact degree_mul_leadingCoeff_inv q hq.ne_zero ▸ degree_eq_one_of_irreducible_of_root this hx
