bump

FltRegular.lean

@@ -6,7 +6,6 @@ import FltRegular.CaseII.Statement
 import FltRegular.FLT5
 import FltRegular.FltRegular
 import FltRegular.MayAssume.Lemmas
-import FltRegular.NumberTheory.AuxLemmas
 import FltRegular.NumberTheory.Cyclotomic.CaseI
 import FltRegular.NumberTheory.Cyclotomic.CyclRat
 import FltRegular.NumberTheory.Cyclotomic.CyclotomicUnits
@@ -15,7 +14,6 @@ import FltRegular.NumberTheory.Cyclotomic.GaloisActionOnCyclo
 import FltRegular.NumberTheory.Cyclotomic.MoreLemmas
 import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
 import FltRegular.NumberTheory.CyclotomicRing
-import FltRegular.NumberTheory.Different
 import FltRegular.NumberTheory.Finrank
 import FltRegular.NumberTheory.GaloisPrime
 import FltRegular.NumberTheory.Hilbert90

FltRegular/NumberTheory/GaloisPrime.lean

@@ -1,11 +1,12 @@
-import FltRegular.NumberTheory.AuxLemmas
 import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 import Mathlib.Data.Set.Card
 import Mathlib.FieldTheory.PurelyInseparable
 import Mathlib.Order.CompletePartialOrder
 import Mathlib.RingTheory.DedekindDomain.Dvr
 import Mathlib.Algebra.Order.Star.Basic
 import Mathlib.RingTheory.SimpleRing.Basic
+import Mathlib.NumberTheory.RamificationInertia
+import Mathlib.Algebra.Lie.OfAssociative
 
 /-!
 # Galois action on primes
@@ -237,15 +238,14 @@ lemma Ideal.ramificationIdxIn_bot : (⊥ : Ideal R).ramificationIdxIn S = 0 := b
 lemma Ideal.inertiaDegIn_bot [Nontrivial R] [IsDomain S] [NoZeroSMulDivisors R S] [IsNoetherian R S]
     [Algebra.IsIntegral R S] [H : (⊥ : Ideal R).IsMaximal] :
     (⊥ : Ideal R).inertiaDegIn S = Module.finrank R S := by
-  delta inertiaDegIn
+  dsimp [inertiaDegIn]
   rw [primesOver_bot]
   have : ({⊥} : Set (Ideal S)).Nonempty := by simp
   rw [dif_pos this, this.choose_spec]
   have hR := not_imp_not.mp (Ring.ne_bot_of_isMaximal_of_not_isField H) rfl
   have hS := isField_of_isIntegral_of_isField' (S := S) hR
   letI : Field R := hR.toField
   letI : Field S := hS.toField
-  have : IsIntegralClosure S R S := isIntegralClosure_self
   rw [← Ideal.map_bot (f := algebraMap R S), ← finrank_quotient_map (R := R) (S := S) ⊥ R S]
   exact inertiaDeg_algebraMap _ _
 
@@ -261,7 +261,7 @@ lemma Ideal.ramificationIdxIn_eq_ramificationIdx [IsGalois K L] (p : Ideal R) (P
   rw [dif_pos this]
   have ⟨σ, hσ⟩ := exists_comap_galRestrict_eq R K L S hP this.choose_spec
   rw [← hσ]
-  exact Ideal.ramificationIdx_comap_eq (galRestrict R K L S σ) p P
+  exact Ideal.ramificationIdx_comap_eq (galRestrict R K L S σ) P
 
 lemma Ideal.inertiaDegIn_eq_inertiaDeg [IsGalois K L] (p : Ideal R) (P : Ideal S)
     (hP : P ∈ primesOver S p) [p.IsMaximal] :
@@ -271,7 +271,7 @@ lemma Ideal.inertiaDegIn_eq_inertiaDeg [IsGalois K L] (p : Ideal R) (P : Ideal S
   rw [dif_pos this]
   have ⟨σ, hσ⟩ := exists_comap_galRestrict_eq R K L S hP this.choose_spec
   rw [← hσ]
-  exact Ideal.inertiaDeg_comap_eq (galRestrict R K L S σ) p P
+  exact Ideal.inertiaDeg_comap_eq p (galRestrict R K L S σ) P
 
 open Module
 

FltRegular/NumberTheory/KummersLemma/Field.lean

@@ -101,9 +101,10 @@ lemma map_poly : (poly hp hζ u hcong).map (algebraMap (𝓞 K) K) =
 include hu in
 lemma irreducible_map_poly :
     Irreducible ((poly hp hζ u hcong).map (algebraMap (𝓞 K) K)) := by
-  rw [map_poly, ← irreducible_taylor_iff (r := 1 / (ζ - 1))]
-  simp only [taylor, one_div, map_add, LinearMap.coe_mk, AddHom.coe_mk, pow_comp, sub_comp,
-    X_comp, C_comp, add_sub_cancel_right]
+  rw [map_poly]
+  refine Irreducible.of_map (f := algEquivAevalXAddC (1 / (ζ - 1))) ?_
+  simp only [one_div, map_add, algEquivAevalXAddC_apply, map_pow, map_sub, aeval_X, aeval_C,
+    algebraMap_eq, add_sub_cancel_right]
   rw [← sub_neg_eq_add, ← (C : K →+* _).map_neg]
   apply X_pow_sub_C_irreducible_of_prime hpri.out
   intro b hb

FltRegular/NumberTheory/Unramified.lean

@@ -1,6 +1,7 @@
 import FltRegular.NumberTheory.GaloisPrime
 import Mathlib.NumberTheory.KummerDedekind
-import FltRegular.NumberTheory.Different
+import Mathlib.RingTheory.DedekindDomain.Different
+
 /-!
 # Unramified extensions
 
@@ -166,8 +167,8 @@ lemma isUnramifiedAt_of_Separable_minpoly' [Algebra.IsSeparable K L]
     have hxP : aeval x (derivative (minpoly R x)) ∈ P := by
       have : differentIdeal R S ≤ P := by
         rw [← Ideal.dvd_iff_le]
-        exact (dvd_pow_self _ H).trans (pow_sub_one_dvd_differentIdeal R S P _ hpbot
-        (Ideal.dvd_iff_le.mpr <| Ideal.le_pow_ramificationIdx (p := p) (f := algebraMap R S)))
+        exact (dvd_pow_self _ H).trans (pow_sub_one_dvd_differentIdeal R P _ hpbot <|
+          Ideal.dvd_iff_le.mpr <| Ideal.le_pow_ramificationIdx)
       exact this (aeval_derivative_mem_differentIdeal R K L _ hx')
     rw [← Ideal.Quotient.eq_zero_iff_mem, ← Ideal.Quotient.algebraMap_eq] at hxP
 

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dc72dcdb8e97b3c56bd70f06f043ed2dee3258e6",
+   "rev": "eb6c831c05bc6ca6d37454ca97531a9b780dfcb5",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9d502188e7df20d93aded2b312b28259ff1da308",
+   "rev": "d27f22898a74975360dd1387155c6031b501a90b",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,