chore(Algebra/Polynomial/Splits): deprecate Splits.splits and splits_iff_splits (leanprover-community#33934)

After the big refactor of `Polynomial.Splits`, there were two clunky lemmas without good names. This PR deprecates them.

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

Author: tb65536

Mathlib/Algebra/Polynomial/Splits.lean

@@ -462,7 +462,7 @@ theorem splits_prod_iff {ι : Type*} {f : ι → R[X]} {s : Finset ι} (hf : ∀
   ⟨fun h _ hx ↦ h.of_dvd (Finset.prod_ne_zero_iff.mpr hf) (Finset.dvd_prod_of_mem f hx),
     Splits.prod⟩
 
--- Todo: Remove or fix name once `Splits` is gone.
+@[deprecated "Use `Splits.degree_le_one_of_irreducible` instead." (since := "2026-01-13")]
 theorem Splits.splits (hf : Splits f) :
     f = 0 ∨ ∀ {g : R[X]}, Irreducible g → g ∣ f → degree g ≤ 1 :=
   or_iff_not_imp_left.mpr fun hf0 _ hg hgf ↦ degree_le_of_natDegree_le <|
@@ -588,11 +588,11 @@ theorem Splits.of_degree_eq_two {x : R} (h₁ : f.degree = 2) (h₂ : f.eval x =
   Splits.of_natDegree_eq_two (natDegree_eq_of_degree_eq_some h₁) h₂
 
 open UniqueFactorizationMonoid in
--- Todo: Remove or fix name.
+@[deprecated "Use `Splits.degree_eq_one_of_irreducible` instead." (since := "2026-01-13")]
 theorem splits_iff_splits {f : R[X]} :
     Splits f ↔ f = 0 ∨ ∀ {g : R[X]}, Irreducible g → g ∣ f → degree g = 1 := by
-  refine ⟨fun hf ↦ hf.splits.imp_right (forall₃_imp fun g hg hgf ↦
-    (le_antisymm · (Nat.WithBot.one_le_iff_zero_lt.mpr hg.degree_pos))), ?_⟩
+  refine ⟨fun hf ↦ or_iff_not_imp_left.mpr fun h0 g hg hgf ↦
+    (hf.of_dvd h0 hgf).degree_eq_one_of_irreducible hg, ?_⟩
   rintro (rfl | hf)
   · aesop
   classical

Mathlib/FieldTheory/AbelRuffini.lean

@@ -114,9 +114,9 @@ theorem gal_X_pow_sub_C_isSolvable_aux (n : ℕ) (a : F)
   have mem_range : ∀ {c : (X ^ n - C a).SplittingField},
       (c ^ n = 1 → (∃ d, algebraMap F (X ^ n - C a).SplittingField d = c)) := fun {c} hc =>
     RingHom.mem_range.mp (minpoly.mem_range_of_degree_eq_one F c
-      ((splits_iff_splits.mp h).resolve_left (map_ne_zero hn''')
-      (minpoly.irreducible ((SplittingField.instNormal (X ^ n - C a)).isIntegral c))
-      (minpoly.dvd F c (by rwa [map_id, map_sub, sub_eq_zero, aeval_X_pow, aeval_one]))))
+      (Splits.degree_eq_one_of_irreducible (h.of_dvd (map_ne_zero hn''')
+        (minpoly.dvd F c (by rwa [map_id, map_sub, sub_eq_zero, aeval_X_pow, aeval_one])))
+          (minpoly.irreducible ((SplittingField.instNormal (X ^ n - C a)).isIntegral c))))
   apply isSolvable_of_comm
   intro σ τ
   ext b hb

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

@@ -187,21 +187,25 @@ theorem exists_aeval_eq_zero {R : Type*} [CommSemiring R] [IsAlgClosed k] [Algeb
     [FaithfulSMul R k] (p : R[X]) (hp : p.degree ≠ 0) : ∃ x : k, p.aeval x = 0 :=
   exists_aeval_eq_zero_of_injective _ (FaithfulSMul.algebraMap_injective ..) _ hp
 
-
 /--
 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 ↦ splits_iff_splits.mpr <| 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
+  replace H (p : k[X]) (hp : Irreducible p) : ∃ x, p.eval x = 0 := by
+    obtain ⟨x, hx⟩ := H (p * C (leadingCoeff p)⁻¹) (monic_mul_leadingCoeff_inv hp.ne_zero)
+      (irreducible_mul_leadingCoeff_inv.mpr hp)
+    exact ⟨x, by simpa [hp.ne_zero] using hx⟩
+  refine ⟨fun p ↦ ?_⟩
+  by_cases hp0 : p = 0
+  · simp [hp0]
+  obtain ⟨u, hu⟩ := UniqueFactorizationMonoid.factors_prod hp0
+  rw [← hu]
+  refine (Splits.multisetProd fun f hf ↦ ?_).mul u.isUnit.splits
+  let h := UniqueFactorizationMonoid.irreducible_of_factor f hf
+  obtain ⟨x, hx⟩ := H f h
+  exact Splits.of_degree_eq_one (degree_eq_one_of_irreducible_of_root h hx)
 
 theorem of_ringEquiv (k' : Type u) [Field k'] (e : k ≃+* k')
     [IsAlgClosed k] : IsAlgClosed k' := by

Mathlib/FieldTheory/IsSepClosed.lean

@@ -183,18 +183,19 @@ variable (k) {K}
 
 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 ↦ splits_iff_splits.mpr <| Or.inr ?_⟩
-  intro q hq 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
+  replace H (p : k[X]) (hp : Irreducible p) (hs : Separable p) : ∃ x, p.eval x = 0 := by
+    obtain ⟨x, hx⟩ := H (p * C (leadingCoeff p)⁻¹) (monic_mul_leadingCoeff_inv hp.ne_zero)
+      (irreducible_mul_leadingCoeff_inv.mpr hp) (hs.mul_unit (by aesop))
+    exact ⟨x, by simpa [hp.ne_zero] using hx⟩
+  refine ⟨fun p hp ↦ ?_⟩
+  by_cases hp0 : p = 0
+  · simp [hp0]
+  obtain ⟨u, hu⟩ := UniqueFactorizationMonoid.factors_prod hp0
+  rw [← hu]
+  refine (Splits.multisetProd fun f hf ↦ ?_).mul u.isUnit.splits
+  let h := UniqueFactorizationMonoid.irreducible_of_factor f hf
+  obtain ⟨x, hx⟩ := H f h (hp.of_dvd (UniqueFactorizationMonoid.dvd_of_mem_factors hf))
+  exact Splits.of_degree_eq_one (degree_eq_one_of_irreducible_of_root h hx)
 
 theorem degree_eq_one_of_irreducible [IsSepClosed k] {p : k[X]}
     (hp : Irreducible p) (hsep : p.Separable) : p.degree = 1 :=

Mathlib/FieldTheory/Normal/Defs.lean

@@ -130,10 +130,9 @@ def AlgHom.restrictNormalAux [h : Normal F E] :
       rintro x ⟨y, ⟨z, hy⟩, hx⟩
       rw [← hx, ← hy]
       apply minpoly.mem_range_of_degree_eq_one E
-      refine
-        Or.resolve_left (splits_iff_splits.mp (h.splits z))
-          (map_ne_zero (minpoly.ne_zero (h.isIntegral z))) (minpoly.irreducible ?_)
-          (minpoly.dvd E _ (by simp [aeval_algHom_apply]))
+      refine ((h.splits z).of_dvd (map_ne_zero (minpoly.ne_zero (h.isIntegral z)))
+        (minpoly.dvd E _ (by simp [aeval_algHom_apply]))).degree_eq_one_of_irreducible
+        (minpoly.irreducible ?_)
       simp only [AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom]
       suffices IsIntegral F _ by exact this.tower_top
       exact ((h.isIntegral z).map <| toAlgHom F E K₁).map ϕ⟩

Mathlib/FieldTheory/SeparableDegree.lean

@@ -892,12 +892,15 @@ end Field
 if and only if every separable degree one polynomial splits. -/
 theorem perfectField_iff_splits_of_natSepDegree_eq_one (F : Type*) [Field F] :
     PerfectField F ↔ ∀ f : F[X], f.natSepDegree = 1 → Splits f := by
-  refine ⟨fun ⟨h⟩ f hf ↦ splits_iff_splits.2 <| or_iff_not_imp_left.2 fun hn g hg hd ↦ ?_,
-      fun h ↦ ?_⟩
-  · have := natSepDegree_le_of_dvd g f hd hn
-    rw [hf, (h hg).natSepDegree_eq_natDegree] at this
-    exact (degree_eq_iff_natDegree_eq_of_pos one_pos).2 <| this.antisymm <|
-      natDegree_pos_iff_degree_pos.2 (degree_pos_of_irreducible hg)
+  refine ⟨fun ⟨h⟩ f hf ↦ ?_, fun h ↦ ?_⟩
+  · have hf0 : f ≠ 0 := by aesop
+    obtain ⟨u, hu⟩ := UniqueFactorizationMonoid.factors_prod hf0
+    rw [← hu]
+    refine (Splits.multisetProd fun g hg ↦ ?_).mul u.isUnit.splits
+    specialize h (UniqueFactorizationMonoid.irreducible_of_factor g hg)
+    have key := natSepDegree_le_of_dvd g f (UniqueFactorizationMonoid.dvd_of_mem_factors hg) hf0
+    rw [h.natSepDegree_eq_natDegree, hf] at key
+    exact Splits.of_natDegree_le_one key
   obtain ⟨p, _⟩ := ExpChar.exists F
   haveI := PerfectRing.ofSurjective F p fun x ↦ by
     obtain ⟨y, hy⟩ := Splits.exists_eval_eq_zero