bump

Author: riccardobrasca

FltRegular/CaseII/AuxLemmas.lean

@@ -11,14 +11,14 @@ open Polynomial
 
 lemma WfDvdMonoid.multiplicity_finite_iff {M : Type*} [CancelCommMonoidWithZero M] [WfDvdMonoid M]
     {x y : M} :
-  multiplicity.Finite x y ↔ ¬IsUnit x ∧ y ≠ 0 := by
+  FiniteMultiplicity x y ↔ ¬IsUnit x ∧ y ≠ 0 := by
   constructor
   · rw [← not_imp_not, Ne, ← not_or, not_not]
     rintro (hx|hy)
     · exact fun ⟨n, hn⟩ ↦ hn (hx.pow _).dvd
     · simp [hy]
   · intro ⟨hx, hy⟩
-    exact multiplicity.finite_of_not_isUnit hx hy
+    exact FiniteMultiplicity.of_not_isUnit hx hy
 
 lemma dvd_iff_emultiplicity_le {M : Type*}
     [CancelCommMonoidWithZero M] [DecidableRel (fun a b : M ↦ a ∣ b)] [UniqueFactorizationMonoid M]
@@ -44,12 +44,12 @@ lemma dvd_iff_emultiplicity_le {M : Type*}
       rw [← pow_one q, pow_dvd_iff_le_emultiplicity]
       have := H q hq
       rw [emultiplicity_mul hq, emultiplicity_mul hq,
-        multiplicity.Finite.emultiplicity_eq_multiplicity (WfDvdMonoid.multiplicity_finite_iff.2
-          ⟨hq.not_unit, hb.2⟩), multiplicity.Finite.emultiplicity_eq_multiplicity
-          (WfDvdMonoid.multiplicity_finite_iff.2 ⟨hq.not_unit, ha.2⟩), multiplicity.Finite.emultiplicity_eq_multiplicity (WfDvdMonoid.multiplicity_finite_iff.2
+        FiniteMultiplicity.emultiplicity_eq_multiplicity (WfDvdMonoid.multiplicity_finite_iff.2
+          ⟨hq.not_unit, hb.2⟩), FiniteMultiplicity.emultiplicity_eq_multiplicity
+          (WfDvdMonoid.multiplicity_finite_iff.2 ⟨hq.not_unit, ha.2⟩), FiniteMultiplicity.emultiplicity_eq_multiplicity (WfDvdMonoid.multiplicity_finite_iff.2
           ⟨hq.not_unit, hq.ne_zero⟩), multiplicity_self, ← Nat.cast_add, ← Nat.cast_add,
           Nat.cast_le, add_comm, add_le_add_iff_left] at this
-      rwa [multiplicity.Finite.emultiplicity_eq_multiplicity
+      rwa [FiniteMultiplicity.emultiplicity_eq_multiplicity
         (WfDvdMonoid.multiplicity_finite_iff.2 ⟨hq.not_unit, hb.2⟩), Nat.cast_one,
         Nat.one_le_cast]
 
@@ -64,25 +64,25 @@ lemma pow_dvd_pow_iff_dvd {M : Type*} [CancelCommMonoidWithZero M] [UniqueFactor
   rw [dvd_iff_emultiplicity_le ha, dvd_iff_emultiplicity_le ha']
   refine forall₂_congr (fun p hp ↦ ⟨fun h ↦ ?_, fun h ↦  ?_⟩)
   · rw [emultiplicity_pow hp, emultiplicity_pow hp,
-      multiplicity.Finite.emultiplicity_eq_multiplicity
+      FiniteMultiplicity.emultiplicity_eq_multiplicity
       (WfDvdMonoid.multiplicity_finite_iff.2 ⟨hp.not_unit, ha⟩),
-      multiplicity.Finite.emultiplicity_eq_multiplicity
+      FiniteMultiplicity.emultiplicity_eq_multiplicity
       (WfDvdMonoid.multiplicity_finite_iff.2 ⟨hp.not_unit, hb⟩), ← Nat.cast_mul, ← Nat.cast_mul,
       Nat.cast_le] at h
-    rw [multiplicity.Finite.emultiplicity_eq_multiplicity
+    rw [FiniteMultiplicity.emultiplicity_eq_multiplicity
       (WfDvdMonoid.multiplicity_finite_iff.2 ⟨hp.not_unit, ha⟩),
-      multiplicity.Finite.emultiplicity_eq_multiplicity
+      FiniteMultiplicity.emultiplicity_eq_multiplicity
       (WfDvdMonoid.multiplicity_finite_iff.2 ⟨hp.not_unit, hb⟩), Nat.cast_le]
     exact le_of_nsmul_le_nsmul_right h' h
   · rw [emultiplicity_pow hp, emultiplicity_pow hp,
-      multiplicity.Finite.emultiplicity_eq_multiplicity
+      FiniteMultiplicity.emultiplicity_eq_multiplicity
       (WfDvdMonoid.multiplicity_finite_iff.2 ⟨hp.not_unit, ha⟩),
-      multiplicity.Finite.emultiplicity_eq_multiplicity
+      FiniteMultiplicity.emultiplicity_eq_multiplicity
       (WfDvdMonoid.multiplicity_finite_iff.2 ⟨hp.not_unit, hb⟩), ← Nat.cast_mul, ← Nat.cast_mul,
       Nat.cast_le]
-    rw [multiplicity.Finite.emultiplicity_eq_multiplicity
+    rw [FiniteMultiplicity.emultiplicity_eq_multiplicity
       (WfDvdMonoid.multiplicity_finite_iff.2 ⟨hp.not_unit, ha⟩),
-      multiplicity.Finite.emultiplicity_eq_multiplicity
+      FiniteMultiplicity.emultiplicity_eq_multiplicity
       (WfDvdMonoid.multiplicity_finite_iff.2 ⟨hp.not_unit, hb⟩),
       Nat.cast_le] at h
     exact Nat.mul_le_mul_left x h
@@ -173,8 +173,8 @@ lemma exists_not_dvd_spanSingleton_eq {R : Type*} [CommRing R] [IsDomain R] [IsD
   by_cases h : s = 0
   · rw [div_eq_iff hJ', h, IsLocalization.mk'_zero, spanSingleton_zero, zero_mul] at ha
     exact hI' ha
-  obtain ⟨n, hn⟩ := multiplicity.finite_of_not_isUnit hx.not_unit h
-  obtain ⟨m, hm⟩ := multiplicity.finite_of_not_isUnit hx.not_unit (nonZeroDivisors.ne_zero t.prop)
+  obtain ⟨n, hn⟩ := FiniteMultiplicity.of_not_isUnit hx.not_unit h
+  obtain ⟨m, hm⟩ := FiniteMultiplicity.of_not_isUnit hx.not_unit (nonZeroDivisors.ne_zero t.prop)
   rw [IsFractionRing.mk'_eq_div] at ha
   refine this (n + m + 1) (Nat.le_add_left 1 (n + m)) ⟨s, t, ?_, ?_, ha.symm⟩
   · intro hs

FltRegular/CaseII/Statement.lean

@@ -32,17 +32,17 @@ lemma not_exists_solution' :
   obtain ⟨m, z, hm, hz'', rfl⟩ :
     ∃ m z', 1 ≤ m ∧ ¬((hζ.unit' : 𝓞 K) - 1 ∣ z') ∧ z = ((hζ.unit' : 𝓞 K) - 1) ^ m * z' := by
     classical
-    have H : multiplicity.Finite ((hζ.unit' : 𝓞 K) - 1) z := multiplicity.finite_of_not_isUnit
+    have H : FiniteMultiplicity ((hζ.unit' : 𝓞 K) - 1) z := FiniteMultiplicity.of_not_isUnit
       hζ.zeta_sub_one_prime'.not_unit hz'
     obtain ⟨z', h⟩ := pow_multiplicity_dvd ((hζ.unit' : 𝓞 K) - 1) z
     refine ⟨_, _, ?_, ?_, h⟩
-    · rwa [← Nat.cast_le (α := ENat), ← multiplicity.Finite.emultiplicity_eq_multiplicity H,
+    · rwa [← Nat.cast_le (α := ENat), ← FiniteMultiplicity.emultiplicity_eq_multiplicity H,
         ← pow_dvd_iff_le_emultiplicity, pow_one]
     · intro h'
       have := mul_dvd_mul_left (((hζ.unit' : 𝓞 K) - 1) ^ (multiplicity ((hζ.unit' : 𝓞 K) - 1) z)) h'
       rw [← pow_succ, ← h] at this
       refine not_pow_dvd_of_emultiplicity_lt ?_ this
-      rw [multiplicity.Finite.emultiplicity_eq_multiplicity H, Nat.cast_lt]
+      rw [FiniteMultiplicity.emultiplicity_eq_multiplicity H, Nat.cast_lt]
       exact Nat.lt_succ_self _
   refine not_exists_solution hp hreg hζ hm ⟨x, y, z, 1, hy, hz'', ?_⟩
   rwa [Units.val_one, one_mul]

FltRegular/NumberTheory/GaloisPrime.lean

@@ -224,8 +224,7 @@ def Ideal.ramificationIdxIn (p : Ideal R) : ℕ :=
 open scoped Classical in
 noncomputable
 def Ideal.inertiaDegIn (p : Ideal R) [p.IsMaximal] : ℕ :=
-  if h : (primesOver S p).Nonempty then
-    Ideal.inertiaDeg (algebraMap R S) p h.choose else 0
+  if h : (primesOver S p).Nonempty then Ideal.inertiaDeg p h.choose else 0
 
 variable (R)
 
@@ -268,7 +267,7 @@ lemma Ideal.ramificationIdxIn_eq_ramificationIdx [IsGalois K L] (p : Ideal R) (P
 
 lemma Ideal.inertiaDegIn_eq_inertiaDeg [IsGalois K L] (p : Ideal R) (P : Ideal S)
     (hP : P ∈ primesOver S p) [p.IsMaximal] :
-    p.inertiaDegIn S = Ideal.inertiaDeg (algebraMap R S) p P := by
+    p.inertiaDegIn S = Ideal.inertiaDeg p P := by
   delta inertiaDegIn
   have : (primesOver S p).Nonempty := ⟨P, hP⟩
   rw [dif_pos this]

FltRegular/NumberTheory/Hilbert92.lean

@@ -6,7 +6,8 @@ import Mathlib.Data.Int.Star
 import Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
 import Mathlib.Order.CompletePartialOrder
 import Mathlib.RingTheory.Henselian
-import Mathlib.LinearAlgebra.Dimension.Torsion
+import Mathlib.LinearAlgebra.Dimension.Torsion.Basic
+import Mathlib.LinearAlgebra.Dimension.Torsion.Finite
 import Mathlib.GroupTheory.FiniteAbelian.Basic
 
 open scoped NumberField nonZeroDivisors
@@ -399,7 +400,8 @@ open multiplicity in
 theorem padicValNat_dvd_iff_le' {p : ℕ} (hp : p ≠ 1) {a n : ℕ} (ha : a ≠ 0) :
     p ^ n ∣ a ↔ n ≤ padicValNat p a := by
   rw [pow_dvd_iff_le_emultiplicity, padicValNat_def' hp ha.bot_lt]
-  exact ⟨fun h ↦ Finite.le_multiplicity_of_le_emultiplicity (Nat.multiplicity_finite_iff.2
+  exact ⟨fun h ↦ FiniteMultiplicity.le_multiplicity_of_le_emultiplicity
+    (Nat.finiteMultiplicity_iff.2
     ⟨hp, Nat.zero_lt_of_ne_zero ha⟩) h, fun h ↦ le_emultiplicity_of_le_multiplicity h⟩
 
 theorem padicValNat_dvd_iff' {p : ℕ} (hp : p ≠ 1) (n : ℕ) (a : ℕ) :

FltRegular/NumberTheory/Hilbert94.lean

@@ -18,6 +18,7 @@ variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B] [Algebra A L] [Al
     [Algebra B L] [IsScalarTower A B L] [IsScalarTower A K L] [IsFractionRing A K]
     [IsIntegralClosure B A L]
 
+set_option synthInstance.maxHeartbeats 160000 in
 include hσ in
 lemma comap_span_galRestrict_eq_of_cyclic (β : B) (η : Bˣ) (hβ : η * (galRestrict A K L B σ) β = β)
     (σ' : L ≃ₐ[K] L) :

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "099b90e374ba73983c3fda87595be625f1931669",
+   "rev": "e837a30396accd8c8cf8b71e85199412f5a05d2c",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "67d092e380faf850fd6a1febf81c27fb33c6c5c8",
+   "rev": "3c9302f1c89690f1c68477fe9f31c228847b7c46",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -115,10 +115,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8b6048aa0a4a4b6bcf83597802d8dee734e64b7e",
+   "rev": "43bcb1964528411e47bfa4edd0c87d1face1fce4",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c016aa9938c4cedc9b7066099f99bcae1b1af625",
+   "rev": "9e583efcea920afa13ee2a53069821a2297a94c0",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",