refactor(Algebra/Polynomial/Splits): continue deprecation (leanprover-community#32752)

This PR continues the deprecation in Splits.lean as we move over to the new API in Factors.lean.

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

Author: tb65536

Mathlib/Algebra/Polynomial/Factors.lean

@@ -376,6 +376,28 @@ theorem Splits.adjoin_rootSet_eq_range {A B : Type*} [CommRing A] [CommRing B]
   rw [← hf.image_rootSet g, Algebra.adjoin_image, ← Algebra.map_top]
   exact (Subalgebra.map_injective g.injective).eq_iff
 
+theorem Splits.coeff_zero_eq_leadingCoeff_mul_prod_roots (hf : Splits f) :
+    f.coeff 0 = (-1) ^ f.natDegree * f.leadingCoeff * f.roots.prod := by
+  conv_lhs => rw [hf.eq_prod_roots]
+  simp [coeff_zero_eq_eval_zero, eval_multiset_prod, hf.natDegree_eq_card_roots,
+    mul_assoc, mul_left_comm]
+
+/-- If `f` is a monic polynomial that splits, then `coeff f 0` equals the product of the roots. -/
+theorem Splits.coeff_zero_eq_prod_roots_of_monic (hf : Splits f) (hm : Monic f) :
+    coeff f 0 = (-1) ^ f.natDegree * f.roots.prod := by
+  simp [hf.coeff_zero_eq_leadingCoeff_mul_prod_roots, hm]
+
+theorem Splits.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff (hf : Splits f) :
+    f.nextCoeff = -f.leadingCoeff * f.roots.sum := by
+  conv_lhs => rw [hf.eq_prod_roots]
+  simp [Multiset.sum_map_neg', monic_X_sub_C, Monic.nextCoeff_multiset_prod]
+
+/-- If `f` is a monic polynomial that splits, then `f.nextCoeff` equals the negative of the sum
+of the roots. -/
+theorem Splits.nextCoeff_eq_neg_sum_roots_of_monic (hf : Splits f) (hm : Monic f) :
+    f.nextCoeff = -f.roots.sum := by
+  simp [hf.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff,hm]
+
 theorem splits_X_sub_C_mul_iff {a : R} : Splits ((X - C a) * f) ↔ Splits f := by
   refine ⟨fun hf ↦ ?_, ((Splits.X_sub_C _).mul ·)⟩
   by_cases hf₀ : f = 0
@@ -518,6 +540,18 @@ theorem Splits.natDegree_eq_one_of_irreducible {f : R[X]} (hf : Splits f)
     (h : Irreducible f) : natDegree f = 1 :=
   natDegree_eq_of_degree_eq_some (hf.degree_eq_one_of_irreducible h)
 
+theorem Splits.eval_derivative_eq_eval_mul_sum (hf : Splits f) {x : R} (hx : f.eval x ≠ 0) :
+    f.derivative.eval x = f.eval x * (f.roots.map fun z ↦ 1 / (x - z)).sum := by
+  classical
+  simp only [hf.eval_derivative, hf.eval_eq_prod_roots, ← Multiset.sum_map_mul_left, mul_assoc]
+  refine congr_arg Multiset.sum (Multiset.map_congr rfl fun z hz ↦ ?_)
+  rw [← Multiset.prod_map_erase hz, mul_one_div, mul_div_cancel_left₀]
+  aesop (add simp sub_eq_zero)
+
+theorem Splits.eval_derivative_div_eval_of_ne_zero (hf : Splits f) {x : R} (hx : f.eval x ≠ 0) :
+    f.derivative.eval x / f.eval x = (f.roots.map fun z ↦ 1 / (x - z)).sum := by
+  rw [hf.eval_derivative_eq_eval_mul_sum hx, mul_div_cancel_left₀ _ hx]
+
 theorem Splits.mem_subfield_of_isRoot (F : Subfield R) {f : F[X]} (hf : Splits f) (hf0 : f ≠ 0)
     {x : R} (hx : (f.map F.subtype).IsRoot x) : x ∈ F := by
   simpa using hf.mem_range_of_isRoot hf0 hx

Mathlib/Algebra/Polynomial/Splits.lean

@@ -285,48 +285,25 @@ alias eval_derivative_of_splits := Splits.eval_derivative
 @[deprecated (since := "2025-12-08")]
 alias aeval_root_derivative_of_splits := Splits.eval_root_derivative
 
-theorem eval_derivative_eq_eval_mul_sum_of_splits {p : K[X]} {x : K}
-    (h : p.Splits) (hx : p.eval x ≠ 0) :
-    p.derivative.eval x = p.eval x * (p.roots.map fun z ↦ 1 / (x - z)).sum := by
-  classical
-  suffices p.roots.map (fun z ↦ p.leadingCoeff * ((p.roots.erase z).map (fun w ↦ x - w) ).prod) =
-      p.roots.map fun i ↦ p.leadingCoeff * ((x - i)⁻¹ * (p.roots.map (fun z ↦ x - z)).prod) by
-    nth_rw 2 [Splits.eq_prod_roots h]
-    simp [h.eval_derivative, ← Multiset.sum_map_mul_left, this, eval_multiset_prod,
-      mul_comm, mul_left_comm]
-  refine Multiset.map_congr rfl fun z hz ↦ ?_
-  rw [← Multiset.prod_map_erase hz, inv_mul_cancel_left₀]
-  aesop (add simp sub_eq_zero)
-
-theorem eval_derivative_div_eval_of_ne_zero_of_splits {p : K[X]} {x : K}
-    (h : p.Splits) (hx : p.eval x ≠ 0) :
-    p.derivative.eval x / p.eval x = (p.roots.map fun z ↦ 1 / (x - z)).sum := by
-  rw [eval_derivative_eq_eval_mul_sum_of_splits h hx]
-  exact mul_div_cancel_left₀ _ hx
-
-theorem coeff_zero_eq_leadingCoeff_mul_prod_roots_of_splits {P : K[X]}
-    (hP : P.Splits) :
-    P.coeff 0 = (-1) ^ P.natDegree * P.leadingCoeff * P.roots.prod := by
-  nth_rw 1 [hP.eq_prod_roots]
-  simp only [coeff_zero_eq_eval_zero, eval_mul, eval_C, eval_multiset_prod, Function.comp_apply,
-    Multiset.map_map, eval_sub, eval_X, zero_sub, Multiset.prod_map_neg]
-  grind [splits_iff_card_roots]
-
-/-- If `P` is a monic polynomial that splits, then `coeff P 0` equals the product of the roots. -/
-theorem coeff_zero_eq_prod_roots_of_monic_of_splits {P : K[X]} (hmo : P.Monic)
-    (hP : P.Splits) : coeff P 0 = (-1) ^ P.natDegree * P.roots.prod := by
-  simp [hmo, coeff_zero_eq_leadingCoeff_mul_prod_roots_of_splits hP]
-
-theorem nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splits {P : K[X]}
-    (hP : P.Splits) : P.nextCoeff = -P.leadingCoeff * P.roots.sum := by
-  nth_rw 1 [Splits.eq_prod_roots hP]
-  simp [Multiset.sum_map_neg', monic_X_sub_C, Monic.nextCoeff_multiset_prod]
-
-/-- If `P` is a monic polynomial that splits, then `P.nextCoeff` equals the negative of the sum
-of the roots. -/
-theorem nextCoeff_eq_neg_sum_roots_of_monic_of_splits {P : K[X]} (hmo : P.Monic)
-    (hP : P.Splits) : P.nextCoeff = -P.roots.sum := by
-  simp [hmo, nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splits hP]
+@[deprecated (since := "2025-12-12")]
+alias eval_derivative_eq_eval_mul_sum_of_splits := Splits.eval_derivative_eq_eval_mul_sum
+
+@[deprecated (since := "2025-12-12")]
+alias eval_derivative_div_eval_of_ne_zero_of_splits := Splits.eval_derivative_div_eval_of_ne_zero
+
+@[deprecated (since := "2025-12-12")]
+alias coeff_zero_eq_leadingCoeff_mul_prod_roots_of_splits :=
+  Splits.coeff_zero_eq_leadingCoeff_mul_prod_roots
+
+@[deprecated (since := "2025-12-12")]
+alias coeff_zero_eq_prod_roots_of_monic_of_splits := Splits.coeff_zero_eq_prod_roots_of_monic
+
+@[deprecated (since := "2025-12-12")]
+alias nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splits :=
+  Splits.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff
+
+@[deprecated (since := "2025-12-12")]
+alias nextCoeff_eq_neg_sum_roots_of_monic_of_splits := Splits.nextCoeff_eq_neg_sum_roots_of_monic
 
 @[deprecated (since := "2025-10-08")]
 alias prod_roots_eq_coeff_zero_of_monic_of_splits := coeff_zero_eq_prod_roots_of_monic_of_splits

Mathlib/Analysis/Complex/Polynomial/GaussLucas.lean

@@ -86,7 +86,7 @@ theorem eq_centerMass_of_eval_derivative_eq_zero (hP : 0 < P.degree)
     _ = conj (P.roots.map fun x ↦ 1 / (z - x)).sum := by
       simp only [Finset.sum_multiset_map_count, P.count_roots, s]
     _ = 0 := by
-      rw [← eval_derivative_div_eval_of_ne_zero_of_splits (IsAlgClosed.splits _) hzP]
+      rw [← (IsAlgClosed.splits _).eval_derivative_div_eval_of_ne_zero hzP]
       simp [hz]
 
 /-- *Gauss-Lucas Theorem*: if $P$ is a nonconstant polynomial with complex coefficients,

Mathlib/Analysis/Normed/Unbundled/SpectralNorm.lean

@@ -963,7 +963,7 @@ theorem spectralNorm_eq_norm_coeff_zero_rpow (x : L) :
     ← @spectralNorm_extends K _ L _ _ ((minpoly K x).coeff 0),
     @spectralNorm.eq_of_tower K _ E _ _ L, ← spectralMulAlgNorm_def,
     ← spectralMulAlgNorm_def, Polynomial.coeff_zero_of_isScalarTower,
-    Polynomial.coeff_zero_eq_prod_roots_of_monic_of_splits _ hspl, map_mul, map_pow,
+    hspl.coeff_zero_eq_prod_roots_of_monic _, map_mul, map_pow,
     map_neg_eq_map, map_one, one_pow, one_mul, spectralNorm_pow_natDegree_eq_prod_roots _ _ x]
   · simp [monic_mapAlg_iff, minpoly.monic (Algebra.IsAlgebraic.isAlgebraic x).isIntegral]
   · exact_mod_cast (minpoly.natDegree_pos (Algebra.IsIntegral.isIntegral x)).ne'

Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean

@@ -80,7 +80,7 @@ theorem mem_spectrum_iff_isRoot_charpoly {r : K} : r ∈ spectrum K A ↔ IsRoot
 theorem det_eq_prod_roots_charpoly_of_splits (hAps : A.charpoly.Splits) :
     A.det = (Matrix.charpoly A).roots.prod := by
   rw [det_eq_sign_charpoly_coeff, ← charpoly_natDegree_eq_dim A,
-    Polynomial.coeff_zero_eq_prod_roots_of_monic_of_splits A.charpoly_monic hAps, ← mul_assoc,
+    hAps.coeff_zero_eq_prod_roots_of_monic A.charpoly_monic, ← mul_assoc,
     ← pow_two, pow_right_comm, neg_one_sq, one_pow, one_mul]
 
 theorem trace_eq_sum_roots_charpoly_of_splits (hAps : A.charpoly.Splits) :
@@ -90,7 +90,7 @@ theorem trace_eq_sum_roots_charpoly_of_splits (hAps : A.charpoly.Splits) :
       det_eq_one_of_card_eq_zero (Fintype.card_eq_zero_iff.2 h), Polynomial.roots_one,
       Multiset.empty_eq_zero, Multiset.sum_zero]
   · rw [trace_eq_neg_charpoly_nextCoeff, neg_eq_iff_eq_neg,
-      ← Polynomial.nextCoeff_eq_neg_sum_roots_of_monic_of_splits A.charpoly_monic hAps]
+      ← hAps.nextCoeff_eq_neg_sum_roots_of_monic A.charpoly_monic]
 
 variable (A)
 

Mathlib/RingTheory/Norm/Basic.lean

@@ -76,7 +76,7 @@ theorem PowerBasis.norm_gen_eq_prod_roots [Algebra R F] (pb : PowerBasis R S)
   have := minpoly.monic pb.isIntegral_gen
   rw [PowerBasis.norm_gen_eq_coeff_zero_minpoly, ← pb.natDegree_minpoly, map_mul,
     ← coeff_map,
-    coeff_zero_eq_prod_roots_of_monic_of_splits (this.map _) hf,
+    hf.coeff_zero_eq_prod_roots_of_monic (this.map _),
     this.natDegree_map, map_pow, ← mul_assoc, ← mul_pow]
   simp only [map_neg, map_one, neg_mul, neg_neg, one_pow, one_mul]
 

Mathlib/RingTheory/Trace/Basic.lean

@@ -90,8 +90,8 @@ theorem PowerBasis.trace_gen_eq_sum_roots [Nontrivial S] (pb : PowerBasis K S)
     (hf : ((minpoly K pb.gen).map (algebraMap K F)).Splits) :
     algebraMap K F (trace K S pb.gen) = ((minpoly K pb.gen).aroots F).sum := by
   rw [PowerBasis.trace_gen_eq_nextCoeff_minpoly, map_neg,
-    ← nextCoeff_map_eq, nextCoeff_eq_neg_sum_roots_of_monic_of_splits
-      ((minpoly.monic (PowerBasis.isIntegral_gen _)).map _) hf,
+    ← nextCoeff_map_eq, hf.nextCoeff_eq_neg_sum_roots_of_monic
+      ((minpoly.monic (PowerBasis.isIntegral_gen _)).map _),
     neg_neg]
 
 namespace IntermediateField.AdjoinSimple