refactor(FieldTheory/IsAlgClosed,IsSepClosed): redefine in terms of Polynomial.Factors (#30869)

This PR redefines `IsAlgClosed` and `IsSepClosed` in terms of `Polynomial.Factors` rather than in terms of `Polynomial.Splits (RingHom.id k)`. This is part of a larger effort to switch over from `Polynomial.Splits` to `Polynomial.Factors`.

Co-authored-by: tb65536 <thomas.l.browning@gmail.com>

Author: tb65536

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

@@ -57,28 +57,31 @@ see `IsAlgClosed.splits_codomain` and `IsAlgClosed.splits_domain`.
 -/
 @[stacks 09GR "The definition of `IsAlgClosed` in mathlib is 09GR (4)"]
 class IsAlgClosed : Prop where
-  splits : ∀ p : k[X], p.Splits <| RingHom.id k
+  factors : ∀ p : k[X], p.Factors
 
 /-- Every polynomial splits in the field extension `f : K →+* k` if `k` is algebraically closed.
 
 See also `IsAlgClosed.splits_domain` for the case where `K` is algebraically closed.
 -/
 theorem IsAlgClosed.splits_codomain {k K : Type*} [Field k] [IsAlgClosed k] [CommRing K]
-    {f : K →+* k} (p : K[X]) : p.Splits f := by
-  convert IsAlgClosed.splits (p.map f); simp [splits_map_iff]
+    {f : K →+* k} (p : K[X]) : p.Splits f :=
+  IsAlgClosed.factors (p.map f)
 
 /-- Every polynomial splits in the field extension `f : K →+* k` if `K` is algebraically closed.
 
 See also `IsAlgClosed.splits_codomain` for the case where `k` is algebraically closed.
 -/
 theorem IsAlgClosed.splits_domain {k K : Type*} [Field k] [IsAlgClosed k] [Field K] {f : k →+* K}
     (p : k[X]) : p.Splits f :=
-  Polynomial.splits_of_splits_id _ <| IsAlgClosed.splits _
+  (IsAlgClosed.factors p).map f
 
 namespace IsAlgClosed
 
 variable {k}
 
+theorem splits [IsAlgClosed k] (p : k[X]) : p.Splits (RingHom.id k) :=
+  (IsAlgClosed.factors p).map (RingHom.id k)
+
 /--
 If `k` is algebraically closed, then every nonconstant polynomial has a root.
 -/

Mathlib/FieldTheory/IsSepClosed.lean

@@ -59,14 +59,18 @@ To show `Polynomial.Splits p f` for an arbitrary ring homomorphism `f`,
 see `IsSepClosed.splits_codomain` and `IsSepClosed.splits_domain`.
 -/
 class IsSepClosed : Prop where
-  splits_of_separable : ∀ p : k[X], p.Separable → (p.Splits <| RingHom.id k)
+  factors_of_separable : ∀ p : k[X], p.Separable → p.Factors
 
 /-- An algebraically closed field is also separably closed. -/
 instance IsSepClosed.of_isAlgClosed [IsAlgClosed k] : IsSepClosed k :=
-  ⟨fun p _ ↦ IsAlgClosed.splits p⟩
+  ⟨fun p _ ↦ IsAlgClosed.factors p⟩
 
 variable {k} {K}
 
+theorem IsSepClosed.splits_of_separable [IsSepClosed k] (p : k[X]) (hp : p.Separable) :
+    p.Splits (RingHom.id k) :=
+  (factors_of_separable p hp).map (RingHom.id k)
+
 /-- Every separable polynomial splits in the field extension `f : k →+* K` if `K` is
 separably closed.
 
@@ -173,7 +177,6 @@ theorem of_exists_root (H : ∀ p : k[X], p.Monic → Irreducible p → Separabl
     IsSepClosed k := by
   refine ⟨fun p hsep ↦ factors_iff_splits.mpr <| 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)⁻¹) :=