English
If a universal property H holds for all monic irreducible separable polynomials p ∈ k[X], then IsSepClosed k.
Русский
Если для всех моничных Ирreducible сепарабельных p ∈ k[X] существует корень, то IsSepClosed k.
LaTeX
$$ (∀ p, p.Monic → Irreducible p → Separable p → ∃ x, p.eval x = 0) ⇒ IsSepClosed k$$
Lean4
theorem of_exists_root (H : ∀ p : k[X], p.Monic → Irreducible p → Separable p → ∃ x, p.eval x = 0) : IsSepClosed k :=
by
refine ⟨fun p hsep ↦ Or.inr ?_⟩
intro q hq hdvd
simp only [map_id] at hdvd
have hlc : IsUnit (leadingCoeff q)⁻¹ := IsUnit.inv <| Ne.isUnit <| leadingCoeff_ne_zero.2 <| Irreducible.ne_zero hq
have hsep' : Separable (q * C (leadingCoeff q)⁻¹) :=
Separable.mul (Separable.of_dvd hsep hdvd) ((separable_C _).2 hlc)
(by
simpa only [← isCoprime_mul_unit_right_right (isUnit_C.2 hlc) q 1, one_mul] using isCoprime_one_right (x := q))
have hirr' := hq
rw [← irreducible_mul_isUnit (isUnit_C.2 hlc)] at hirr'
obtain ⟨x, hx⟩ := H (q * C (leadingCoeff q)⁻¹) (monic_mul_leadingCoeff_inv hq.ne_zero) hirr' hsep'
exact degree_mul_leadingCoeff_inv q hq.ne_zero ▸ degree_eq_one_of_irreducible_of_root hirr' hx
