[Merged by Bors] - refactor: rename Splits.splits_of_dvd to Splits.of_dvd

Mathlib/Algebra/Polynomial/Factors.lean

@@ -431,23 +431,23 @@ theorem splits_mul_iff (hf₀ : f ≠ 0) (hg₀ : g ≠ 0) :
     have := ih (by aesop) hg₀ (f * g) rfl  (splits_X_sub_C_mul_iff.mp h) hn
     aesop
 
-theorem Splits.splits_of_dvd (hg : Splits g) (hg₀ : g ≠ 0) (hfg : f ∣ g) : Splits f := by
+theorem Splits.of_dvd (hg : Splits g) (hg₀ : g ≠ 0) (hfg : f ∣ g) : Splits f := by
   obtain ⟨g, rfl⟩ := hfg
   exact ((splits_mul_iff (by aesop) (by aesop)).mp hg).1
 
 @[deprecated (since := "2025-11-27")]
-alias Splits.of_dvd := Splits.splits_of_dvd
+alias Splits.splits_of_dvd := Splits.of_dvd
 
 theorem splits_prod_iff {ι : Type*} {f : ι → R[X]} {s : Finset ι} (hf : ∀ i ∈ s, f i ≠ 0) :
     (∏ x ∈ s, f x).Splits ↔ ∀ x ∈ s, (f x).Splits :=
-  ⟨fun h _ hx ↦ h.splits_of_dvd (Finset.prod_ne_zero_iff.mpr hf) (Finset.dvd_prod_of_mem f hx),
+  ⟨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.
 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 <|
-    (hf.splits_of_dvd hf0 hgf).natDegree_le_one_of_irreducible hg
+    (hf.of_dvd hf0 hgf).natDegree_le_one_of_irreducible hg
 
 lemma map_sub_sprod_roots_eq_prod_map_eval
     (s : Multiset R) (g : R[X]) (hg : g.Monic) (hg' : g.Splits) :

Mathlib/Algebra/Polynomial/Splits.lean

@@ -142,17 +142,17 @@ alias Splits.def := splits_iff_splits
 alias splits_of_splits_mul := splits_mul_iff
 
 @[deprecated (since := "2025-11-25")]
-alias splits_of_splits_of_dvd := Splits.splits_of_dvd
+alias splits_of_splits_of_dvd := Splits.of_dvd
 
-@[deprecated "Use `Splits.splits_of_dvd` directly." (since := "2025-11-30")]
+@[deprecated "Use `Splits.of_dvd` directly." (since := "2025-11-30")]
 theorem splits_of_splits_gcd_left [DecidableEq K] {f g : K[X]} (hf0 : f ≠ 0)
     (hf : Splits f) : Splits (EuclideanDomain.gcd f g) :=
-  Splits.splits_of_dvd hf hf0 <| EuclideanDomain.gcd_dvd_left f g
+  Splits.of_dvd hf hf0 <| EuclideanDomain.gcd_dvd_left f g
 
-@[deprecated "Use `Splits.splits_of_dvd` directly." (since := "2025-11-30")]
+@[deprecated "Use `Splits.of_dvd` directly." (since := "2025-11-30")]
 theorem splits_of_splits_gcd_right [DecidableEq K] {f g : K[X]} (hg0 : g ≠ 0)
     (hg : Splits g) : Splits (EuclideanDomain.gcd f g) :=
-  Splits.splits_of_dvd hg hg0 <| EuclideanDomain.gcd_dvd_right f g
+  Splits.of_dvd hg hg0 <| EuclideanDomain.gcd_dvd_right f g
 
 @[deprecated (since := "2025-11-30")]
 alias degree_eq_one_of_irreducible_of_splits := Splits.degree_eq_one_of_irreducible

Mathlib/FieldTheory/AbelRuffini.lean

@@ -285,7 +285,7 @@ theorem induction3 {α : solvableByRad F E} {n : ℕ} (hn : n ≠ 0) (hα : P (
     · exact minpoly.ne_zero (isIntegral (α ^ n)) h'
     · exact hn (by rw [← @natDegree_C F, ← h'.2, natDegree_X_pow])
   apply gal_isSolvable_of_splits
-  · exact ⟨(SplittingField.splits (p.comp (X ^ n))).splits_of_dvd (map_ne_zero hp)
+  · exact ⟨(SplittingField.splits (p.comp (X ^ n))).of_dvd (map_ne_zero hp)
       ((map_dvd_map' _).mpr (minpoly.dvd F α (by rw [aeval_comp, aeval_X_pow, minpoly.aeval])))⟩
   · refine gal_isSolvable_tower p (p.comp (X ^ n)) ?_ hα ?_
     · exact Gal.splits_in_splittingField_of_comp _ _ (by rwa [natDegree_X_pow])

Mathlib/FieldTheory/Finite/GaloisField.lean

@@ -301,7 +301,7 @@ theorem nonempty_algHom_of_finrank_dvd (h : Module.finrank F K ∣ Module.finran
   have := Fintype.ofFinite K
   have := Fintype.ofFinite L
   refine ⟨Polynomial.IsSplittingField.lift _ (X ^ Fintype.card K - X) ?_⟩
-  refine (FiniteField.isSplittingField_sub L F).splits.splits_of_dvd ?_ ?_
+  refine (FiniteField.isSplittingField_sub L F).splits.of_dvd ?_ ?_
   · exact map_ne_zero (FiniteField.X_pow_card_sub_X_ne_zero _ Fintype.one_lt_card)
   · rw [Module.card_eq_pow_finrank (K := F), Module.card_eq_pow_finrank (K := F) (V := L)]
     exact (map_dvd_map' _).mpr (dvd_pow_pow_sub_self_of_dvd h)

Mathlib/FieldTheory/Galois/Basic.lean

@@ -530,7 +530,7 @@ theorem of_separable_splitting_field_aux [hFE : FiniteDimensional F E] [sp : p.I
   intro f _
   rw [← @IntermediateField.card_algHom_adjoin_integral K _ E _ _ x E _ (RingHom.toAlgebra f) h]
   · exact Polynomial.Separable.of_dvd ((Polynomial.separable_map (algebraMap F K)).mpr hp) h2
-  · apply sp.splits.splits_of_dvd (Polynomial.map_ne_zero h1)
+  · apply sp.splits.of_dvd (Polynomial.map_ne_zero h1)
     rwa [← f.comp_algebraMap, ← p.map_map, RingHom.algebraMap_toAlgebra, Polynomial.map_dvd_map']
 
 theorem of_separable_splitting_field [sp : p.IsSplittingField F E] (hp : p.Separable) :

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

@@ -301,7 +301,7 @@ theorem IsAlgClosure.of_splits {R K} [CommRing R] [IsDomain R] [Field K] [Algebr
   isAlgebraic := inferInstance
   isAlgClosed := .of_exists_root _ fun _p _ p_irred ↦
     have ⟨g, monic, irred, dvd⟩ := p_irred.exists_dvd_monic_irreducible_of_isIntegral (K := R)
-    ((h g monic irred).splits_of_dvd (map_monic_ne_zero monic) dvd).exists_eval_eq_zero <|
+    ((h g monic irred).of_dvd (map_monic_ne_zero monic) dvd).exists_eval_eq_zero <|
       degree_ne_of_natDegree_ne p_irred.natDegree_pos.ne'
 
 namespace IsAlgClosed

Mathlib/FieldTheory/Isaacs.lean

@@ -44,7 +44,7 @@ theorem nonempty_algHom_of_exist_roots (h : ∀ x : E, ∃ y : K, aeval y (minpo
   let p := (S.prod <| fun x ↦ (minpoly F x).map (algebraMap F K))
   let K' := SplittingField p
   have splits s (hs : s ∈ S) : ((minpoly F s).map (algebraMap F K')).Splits := by
-    apply (SplittingField.splits p).splits_of_dvd (map_ne_zero (Finset.prod_ne_zero_iff.mpr
+    apply (SplittingField.splits p).of_dvd (map_ne_zero (Finset.prod_ne_zero_iff.mpr
       fun _ _ ↦ Polynomial.map_ne_zero (minpoly.ne_zero <| alg.isIntegral.1 _))) ?_
     rw [IsScalarTower.algebraMap_eq F K K', ← Polynomial.map_map, map_dvd_map']
     exact Finset.dvd_prod_of_mem _ hs

Mathlib/FieldTheory/Normal/Closure.lean

@@ -123,7 +123,7 @@ noncomputable def IsNormalClosure.lift [h : IsNormalClosure F K L] {L'} [Field L
     (fun x hx ↦ ⟨isAlgebraic_iff_isIntegral.mp ((h.normal).isAlgebraic x), ?_⟩) this
   obtain ⟨y, hx⟩ := Set.mem_iUnion.mp hx
   by_cases iy : IsIntegral F y
-  · exact (splits y).splits_of_dvd (map_ne_zero (minpoly.ne_zero iy))
+  · exact (splits y).of_dvd (map_ne_zero (minpoly.ne_zero iy))
       ((map_dvd_map' _).mpr (minpoly.dvd F x (mem_rootSet.mp hx).2))
   · simp [minpoly.eq_zero iy] at hx
 
@@ -216,7 +216,7 @@ noncomputable def Algebra.IsAlgebraic.algHomEmbeddingOfSplits [Algebra.IsAlgebra
       obtain ⟨y, hx⟩ := Set.mem_iUnion.mp hx
       refine ⟨isAlgebraic_iff_isIntegral.mp (isAlgebraic_of_mem_rootSet hx), ?_⟩
       by_cases iy : IsIntegral F y
-      · exact (h y).splits_of_dvd (map_ne_zero (minpoly.ne_zero iy))
+      · exact (h y).of_dvd (map_ne_zero (minpoly.ne_zero iy))
           ((map_dvd_map' _).mpr (minpoly.dvd F x (mem_rootSet.mp hx).2))
       · simp [minpoly.eq_zero iy] at hx
   let φ' := (φ.comp <| inclusion normalClosure_le_iSup_adjoin)

Mathlib/FieldTheory/Normal/Defs.lean

@@ -68,7 +68,7 @@ theorem Normal.tower_top_of_normal [h : Normal F E] : Normal K E :=
   normal_iff.2 fun x => by
     obtain ⟨hx, hhx⟩ := h.out x
     rw [algebraMap_eq F K E, ← map_map] at hhx
-    exact ⟨hx.tower_top, hhx.splits_of_dvd (map_ne_zero (map_ne_zero (minpoly.ne_zero hx)))
+    exact ⟨hx.tower_top, hhx.of_dvd (map_ne_zero (map_ne_zero (minpoly.ne_zero hx)))
       ((map_dvd_map' _).mpr (minpoly.dvd_map_of_isScalarTower F K x))⟩
 
 theorem AlgHom.normal_bijective [h : Normal F E] (ϕ : E →ₐ[F] K) : Function.Bijective ϕ :=

Mathlib/FieldTheory/PolynomialGaloisGroup.lean

@@ -219,21 +219,21 @@ def restrictDvd (hpq : p ∣ q) : q.Gal →* p.Gal :=
   if hq : q = 0 then 1
   else
     @restrict F _ p _ _ _
-      ⟨(SplittingField.splits q).splits_of_dvd (map_ne_zero hq) ((map_dvd_map' _).mpr hpq)⟩
+      ⟨(SplittingField.splits q).of_dvd (map_ne_zero hq) ((map_dvd_map' _).mpr hpq)⟩
 
 theorem restrictDvd_def [Decidable (q = 0)] (hpq : p ∣ q) :
     restrictDvd hpq =
       if hq : q = 0 then 1
       else @restrict F _ p _ _ _
-        ⟨(SplittingField.splits q).splits_of_dvd (map_ne_zero hq) ((map_dvd_map' _).mpr hpq)⟩ := by
+        ⟨(SplittingField.splits q).of_dvd (map_ne_zero hq) ((map_dvd_map' _).mpr hpq)⟩ := by
   unfold restrictDvd
   congr
 
 theorem restrictDvd_surjective (hpq : p ∣ q) (hq : q ≠ 0) :
     Function.Surjective (restrictDvd hpq) := by
   classical
   haveI := Fact.mk <|
-    (SplittingField.splits q).splits_of_dvd (map_ne_zero hq) ((map_dvd_map' _).mpr hpq)
+    (SplittingField.splits q).of_dvd (map_ne_zero hq) ((map_dvd_map' _).mpr hpq)
   simpa only [restrictDvd_def, dif_neg hq] using restrict_surjective _ _
 
 variable (p q)
@@ -255,7 +255,7 @@ theorem restrictProd_injective : Function.Injective (restrictProd p q) := by
   rw [rootSet_def, aroots_mul hpq] at hx
   rcases Multiset.mem_add.mp (Multiset.mem_toFinset.mp hx) with h | h
   · haveI : Fact ((p.map (algebraMap F (p * q).SplittingField)).Splits) :=
-      ⟨(SplittingField.splits (p * q)).splits_of_dvd (map_ne_zero hpq)
+      ⟨(SplittingField.splits (p * q)).of_dvd (map_ne_zero hpq)
         ((map_dvd_map' _).mpr (dvd_mul_right p q))⟩
     have key :
       x =
@@ -266,7 +266,7 @@ theorem restrictProd_injective : Function.Injective (restrictProd p q) := by
     rw [key, ← AlgEquiv.restrictNormal_commutes, ← AlgEquiv.restrictNormal_commutes]
     exact congr_arg _ (AlgEquiv.ext_iff.mp hfg.1 _)
   · haveI : Fact ((q.map (algebraMap F (p * q).SplittingField)).Splits) :=
-      ⟨(SplittingField.splits (p * q)).splits_of_dvd (map_ne_zero hpq)
+      ⟨(SplittingField.splits (p * q)).of_dvd (map_ne_zero hpq)
         ((map_dvd_map' _).mpr (dvd_mul_left q p))⟩
     have key :
       x =
@@ -285,12 +285,12 @@ theorem mul_splits_in_splittingField_of_mul {p₁ q₁ p₂ q₂ : F[X]} (hq₁
   apply Splits.mul
   · rw [←
       (SplittingField.lift q₁
-          ((SplittingField.splits _).splits_of_dvd (map_ne_zero (mul_ne_zero hq₁ hq₂))
+          ((SplittingField.splits _).of_dvd (map_ne_zero (mul_ne_zero hq₁ hq₂))
              ((map_dvd_map' _).mpr (dvd_mul_right q₁ q₂)))).comp_algebraMap, ← map_map]
     exact h₁.map _
   · rw [←
       (SplittingField.lift q₂
-          ((SplittingField.splits _).splits_of_dvd (map_ne_zero (mul_ne_zero hq₁ hq₂))
+          ((SplittingField.splits _).of_dvd (map_ne_zero (mul_ne_zero hq₁ hq₂))
              ((map_dvd_map' _).mpr (dvd_mul_left q₂ q₁)))).comp_algebraMap, ← map_map]
     exact h₂.map _
 
@@ -309,7 +309,7 @@ theorem splits_in_splittingField_of_comp (hq : q.natDegree ≠ 0) :
     rw [eval_map_algebraMap, aeval_comp] at hx
     have h_normal : Normal F (r.comp q).SplittingField := SplittingField.instNormal (r.comp q)
     have qx_int := Normal.isIntegral h_normal (aeval x q)
-    exact (h_normal.splits _).splits_of_dvd (map_ne_zero (minpoly.ne_zero (h_normal.isIntegral _)))
+    exact (h_normal.splits _).of_dvd (map_ne_zero (minpoly.ne_zero (h_normal.isIntegral _)))
       ((map_dvd_map' _).mpr ((minpoly.irreducible qx_int).dvd_symm hr (minpoly.dvd F _ hx)))
   have key2 : ∀ {p₁ p₂ : F[X]}, P p₁ → P p₂ → P (p₁ * p₂) := by
     intro p₁ p₂ hp₁ hp₂

Mathlib/FieldTheory/PrimitiveElement.lean

@@ -145,7 +145,7 @@ theorem primitive_element_inf_aux [Algebra.IsSeparable F E] : ∃ γ : E, F⟮α
     · rw [eval_map_algebraMap, minpoly.aeval]
   have h_splits : Splits (h.map ιEE') := by
     rw [← Polynomial.gcd_map]
-    exact (SplittingField.splits _).splits_of_dvd (map_ne_zero map_g_ne_zero)
+    exact (SplittingField.splits _).of_dvd (map_ne_zero map_g_ne_zero)
       (EuclideanDomain.gcd_dvd_right _ _)
   have h_roots : ∀ x ∈ (h.map ιEE').roots, x = ιEE' β := by
     intro x hx

Mathlib/FieldTheory/Separable.lean

@@ -462,7 +462,7 @@ theorem nodup_roots_iff_of_splits {f : F[X]} (hf : f ≠ 0) (h : f.Splits) :
   classical
   refine ⟨(fun hnsep ↦ ?_).mtr, nodup_roots⟩
   rw [Separable, ← gcd_isUnit_iff, isUnit_iff_degree_eq_zero] at hnsep
-  obtain ⟨x, hx⟩ := Splits.exists_eval_eq_zero (Splits.splits_of_dvd h hf (gcd_dvd_left f _)) hnsep
+  obtain ⟨x, hx⟩ := Splits.exists_eval_eq_zero (Splits.of_dvd h hf (gcd_dvd_left f _)) hnsep
   simp_rw [Multiset.nodup_iff_count_le_one, not_forall, not_le]
   exact ⟨x, ((one_lt_rootMultiplicity_iff_isRoot_gcd hf).2 hx).trans_eq f.count_roots.symm⟩
 

Mathlib/FieldTheory/SplittingField/IsSplittingField.lean

@@ -120,7 +120,7 @@ def lift [Algebra K F] (f : K[X]) [IsSplittingField K L f]
     exact Classical.choice (lift_of_splits _ fun y hy =>
       have : aeval y f = 0 := (eval₂_eq_eval_map _).trans <|
         (mem_roots <| map_ne_zero hf0).1 (Multiset.mem_toFinset.mp hy)
-    ⟨IsAlgebraic.isIntegral ⟨f, hf0, this⟩, hf.splits_of_dvd (map_ne_zero hf0)
+    ⟨IsAlgebraic.isIntegral ⟨f, hf0, this⟩, hf.of_dvd (map_ne_zero hf0)
       ((map_dvd_map' _).mpr (minpoly.dvd K y this))⟩)) Algebra.toTop
 
 theorem finiteDimensional (f : K[X]) [IsSplittingField K L f] : FiniteDimensional K L := by

Mathlib/NumberTheory/Cyclotomic/Basic.lean

@@ -501,7 +501,7 @@ theorem splits_X_pow_sub_one [H : IsCyclotomicExtension S K L] (hS : n ∈ S) :
 /-- A cyclotomic extension splits `cyclotomic n K` if `n ∈ S`. -/
 theorem splits_cyclotomic [IsCyclotomicExtension S K L] (hS : n ∈ S) :
     Splits ((cyclotomic n K).map (algebraMap K L)) := by
-  refine (splits_X_pow_sub_one K L hS).splits_of_dvd
+  refine (splits_X_pow_sub_one K L hS).of_dvd
     (map_ne_zero (X_pow_sub_C_ne_zero (NeZero.pos _) _)) ((map_dvd_map' _).mpr ?_)
   use ∏ i ∈ n.properDivisors, Polynomial.cyclotomic i K
   rw [(eq_cyclotomic_iff (NeZero.pos _) _).1 rfl]

Mathlib/RingTheory/Adjoin/Field.lean

@@ -84,7 +84,7 @@ theorem Polynomial.lift_of_splits {F K L : Type*} [Field F] [Field K] [Field L]
     letI := (f : Ks →+* L).toAlgebra
     have H5 : IsIntegral Ks a := H1.tower_top
     have H6 : ((minpoly Ks a).map (algebraMap Ks L)).Splits := by
-      refine Splits.splits_of_dvd H2 (map_ne_zero (minpoly.ne_zero H1)) ?_
+      refine Splits.of_dvd H2 (map_ne_zero (minpoly.ne_zero H1)) ?_
       rw [IsScalarTower.algebraMap_eq F Ks L, ← map_map, map_dvd_map']
       exact minpoly.dvd_map_of_isScalarTower F Ks a
     obtain ⟨y, hy⟩ := H6.exists_eval_eq_zero (by simp [(minpoly.degree_pos H5).ne'])
@@ -146,7 +146,7 @@ variable [Algebra K M] [IsScalarTower R K M] {x : M}
 theorem IsIntegral.minpoly_splits_tower_top' (int : IsIntegral R x) {f : K →+* L}
     (h : Splits ((minpoly R x).map (f.comp <| algebraMap R K))) :
     Splits ((minpoly K x).map f) :=
-  Splits.splits_of_dvd h (map_monic_ne_zero (minpoly.monic int))
+  Splits.of_dvd h (map_monic_ne_zero (minpoly.monic int))
     (by rw [← map_map, map_dvd_map']; exact minpoly.dvd_map_of_isScalarTower R K x)
 
 theorem IsIntegral.minpoly_splits_tower_top [Algebra K L] [Algebra R L] [IsScalarTower R K L]

Mathlib/RingTheory/Invariant/Basic.lean

@@ -491,7 +491,7 @@ lemma Ideal.Quotient.normal [P.IsMaximal] [Q.IsMaximal] :
     rw [Polynomial.aeval_def, ← Polynomial.eval_map, hp, MulSemiringAction.eval_charpoly]
   have := minpoly.dvd _ (algebraMap _ (B ⧸ Q) x) (p := p.map (algebraMap _ (A ⧸ P)))
     (by rw [Polynomial.aeval_map_algebraMap, Polynomial.aeval_algebraMap_apply, H, map_zero])
-  refine Polynomial.Splits.splits_of_dvd ?_ ?_ ((Polynomial.map_dvd_map' _).mpr this)
+  refine Polynomial.Splits.of_dvd ?_ ?_ ((Polynomial.map_dvd_map' _).mpr this)
   · rw [Polynomial.map_map, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq A B,
       ← Polynomial.map_map, hp, MulSemiringAction.charpoly_eq, Polynomial.map_prod]
     exact Polynomial.Splits.prod (fun _ _ ↦ (Polynomial.Splits.X_sub_C _).map _)

Mathlib/RingTheory/Polynomial/IsIntegral.lean

@@ -57,7 +57,7 @@ lemma isIntegral_coeff_of_dvd [IsDomain S] (p : R[X]) (q : S[X]) (hp : p.Monic)
   refine (isIntegral_algHom_iff (IsScalarTower.toAlgHom R S L) (algebraMap S L).injective).mp ?_
   rw [IsScalarTower.coe_toAlgHom', ← coeff_map]
   refine Polynomial.isIntegral_coeff_of_factors _ (by simpa using .algebraMap hq) ?_ ?_ i
-  · refine .splits_of_dvd ?_ ((hp.map _).map _).ne_zero (Polynomial.map_dvd _ H)
+  · refine .of_dvd ?_ ((hp.map _).map _).ne_zero (Polynomial.map_dvd _ H)
     exact SplittingField.splits (p.map (algebraMap R S))
   · intro x hx
     exact ⟨p, hp, by simpa using aeval_eq_zero_of_dvd_aeval_eq_zero (a := x) H (by simp_all)⟩