From a5d9c9d51dabd1dd5e03531926e18fa3aadbabde Mon Sep 17 00:00:00 2001 From: tb65536 Date: Sat, 13 Dec 2025 11:22:46 +1300 Subject: [PATCH 1/2] rename --- Mathlib/Algebra/Polynomial/Factors.lean | 8 ++++---- Mathlib/Algebra/Polynomial/Splits.lean | 10 +++++----- Mathlib/FieldTheory/AbelRuffini.lean | 2 +- Mathlib/FieldTheory/Finite/GaloisField.lean | 2 +- Mathlib/FieldTheory/Galois/Basic.lean | 2 +- Mathlib/FieldTheory/IsAlgClosed/Basic.lean | 2 +- Mathlib/FieldTheory/Isaacs.lean | 2 +- Mathlib/FieldTheory/Normal/Closure.lean | 4 ++-- Mathlib/FieldTheory/Normal/Defs.lean | 2 +- Mathlib/FieldTheory/PolynomialGaloisGroup.lean | 16 ++++++++-------- Mathlib/FieldTheory/PrimitiveElement.lean | 2 +- Mathlib/FieldTheory/Separable.lean | 2 +- .../SplittingField/IsSplittingField.lean | 2 +- Mathlib/NumberTheory/Cyclotomic/Basic.lean | 2 +- Mathlib/RingTheory/Adjoin/Field.lean | 4 ++-- Mathlib/RingTheory/Invariant/Basic.lean | 2 +- Mathlib/RingTheory/Polynomial/IsIntegral.lean | 2 +- 17 files changed, 33 insertions(+), 33 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/Factors.lean b/Mathlib/Algebra/Polynomial/Factors.lean index e593fa00aa8c46..099c159858eb0c 100644 --- a/Mathlib/Algebra/Polynomial/Factors.lean +++ b/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) : diff --git a/Mathlib/Algebra/Polynomial/Splits.lean b/Mathlib/Algebra/Polynomial/Splits.lean index 4b543ac3b555c8..341b1b81519885 100644 --- a/Mathlib/Algebra/Polynomial/Splits.lean +++ b/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_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 diff --git a/Mathlib/FieldTheory/AbelRuffini.lean b/Mathlib/FieldTheory/AbelRuffini.lean index ae3124785e82a1..95029a38dd2377 100644 --- a/Mathlib/FieldTheory/AbelRuffini.lean +++ b/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]) diff --git a/Mathlib/FieldTheory/Finite/GaloisField.lean b/Mathlib/FieldTheory/Finite/GaloisField.lean index 70f9d0e5d868de..a28a76c03b6c0f 100644 --- a/Mathlib/FieldTheory/Finite/GaloisField.lean +++ b/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) diff --git a/Mathlib/FieldTheory/Galois/Basic.lean b/Mathlib/FieldTheory/Galois/Basic.lean index 1a5dfe2a7c5ace..4ae7726b01c541 100644 --- a/Mathlib/FieldTheory/Galois/Basic.lean +++ b/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) : diff --git a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean b/Mathlib/FieldTheory/IsAlgClosed/Basic.lean index 55640564a735ae..0f8496f8849a3d 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/Basic.lean +++ b/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 diff --git a/Mathlib/FieldTheory/Isaacs.lean b/Mathlib/FieldTheory/Isaacs.lean index fc473f4412fb61..dd706ad8d51600 100644 --- a/Mathlib/FieldTheory/Isaacs.lean +++ b/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 diff --git a/Mathlib/FieldTheory/Normal/Closure.lean b/Mathlib/FieldTheory/Normal/Closure.lean index 466ce44bdca42a..d45c3d30b60d28 100644 --- a/Mathlib/FieldTheory/Normal/Closure.lean +++ b/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) diff --git a/Mathlib/FieldTheory/Normal/Defs.lean b/Mathlib/FieldTheory/Normal/Defs.lean index 87fdc9ad60947e..fc62167604afa0 100644 --- a/Mathlib/FieldTheory/Normal/Defs.lean +++ b/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 ϕ := diff --git a/Mathlib/FieldTheory/PolynomialGaloisGroup.lean b/Mathlib/FieldTheory/PolynomialGaloisGroup.lean index de5d8cd82d81d9..1307ba10ae4310 100644 --- a/Mathlib/FieldTheory/PolynomialGaloisGroup.lean +++ b/Mathlib/FieldTheory/PolynomialGaloisGroup.lean @@ -219,13 +219,13 @@ 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 @@ -233,7 +233,7 @@ 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₂ diff --git a/Mathlib/FieldTheory/PrimitiveElement.lean b/Mathlib/FieldTheory/PrimitiveElement.lean index 07e1fce77fd8b8..1c5a6f0932a191 100644 --- a/Mathlib/FieldTheory/PrimitiveElement.lean +++ b/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 diff --git a/Mathlib/FieldTheory/Separable.lean b/Mathlib/FieldTheory/Separable.lean index d84ab1eeaf0c94..fa1efff54fc902 100644 --- a/Mathlib/FieldTheory/Separable.lean +++ b/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⟩ diff --git a/Mathlib/FieldTheory/SplittingField/IsSplittingField.lean b/Mathlib/FieldTheory/SplittingField/IsSplittingField.lean index d52fdf78315544..0e7c8ca05a5ba7 100644 --- a/Mathlib/FieldTheory/SplittingField/IsSplittingField.lean +++ b/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 diff --git a/Mathlib/NumberTheory/Cyclotomic/Basic.lean b/Mathlib/NumberTheory/Cyclotomic/Basic.lean index 773a70b6ff24d9..f73ce27c45e9a2 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Basic.lean +++ b/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] diff --git a/Mathlib/RingTheory/Adjoin/Field.lean b/Mathlib/RingTheory/Adjoin/Field.lean index 9f54d57eeaf046..deade1dd18bc50 100644 --- a/Mathlib/RingTheory/Adjoin/Field.lean +++ b/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] diff --git a/Mathlib/RingTheory/Invariant/Basic.lean b/Mathlib/RingTheory/Invariant/Basic.lean index 0d942e463ac4d1..34ab6b6b4b0f47 100644 --- a/Mathlib/RingTheory/Invariant/Basic.lean +++ b/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 _) diff --git a/Mathlib/RingTheory/Polynomial/IsIntegral.lean b/Mathlib/RingTheory/Polynomial/IsIntegral.lean index 883f9df20570ad..c12dc9745753e5 100644 --- a/Mathlib/RingTheory/Polynomial/IsIntegral.lean +++ b/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)⟩ From 59a017de9a44b0c6cb4b519116eb4a755c6f1047 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Sun, 14 Dec 2025 11:58:46 +1300 Subject: [PATCH 2/2] fix --- Mathlib/Algebra/Polynomial/Splits.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Polynomial/Splits.lean b/Mathlib/Algebra/Polynomial/Splits.lean index 341b1b81519885..77250a0455db65 100644 --- a/Mathlib/Algebra/Polynomial/Splits.lean +++ b/Mathlib/Algebra/Polynomial/Splits.lean @@ -142,7 +142,7 @@ alias Splits.def := splits_iff_splits alias splits_of_splits_mul := splits_mul_iff @[deprecated (since := "2025-11-25")] -alias splits_of_of_dvd := Splits.of_dvd +alias splits_of_splits_of_dvd := Splits.of_dvd @[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)