bump

Author: riccardobrasca

FltRegular/CaseII/AuxLemmas.lean

@@ -6,10 +6,8 @@ variable {K : Type*} {p : ℕ} [Field K] [CharZero K] {ζ : K}
 open scoped nonZeroDivisors
 open Polynomial
 
---TODO: fix the following proofs using new multiplicity API
-
-lemma WfDvdMonoid.multiplicity_finite_iff {M : Type*} [CancelCommMonoidWithZero M] [WfDvdMonoid M]
-    {x y : M} :
+lemma WfDvdMonoid.multiplicity_finite_iff {M : Type*} [CommMonoidWithZero M] [IsCancelMulZero M]
+    [WfDvdMonoid M] {x y : M} :
     FiniteMultiplicity x y ↔ ¬IsUnit x ∧ y ≠ 0 := by
   constructor
   · rw [Ne, ← not_or, imp_not_comm]
@@ -20,7 +18,7 @@ lemma WfDvdMonoid.multiplicity_finite_iff {M : Type*} [CancelCommMonoidWithZero
     exact FiniteMultiplicity.of_not_isUnit hx hy
 
 lemma dvd_iff_emultiplicity_le {M : Type*}
-    [CancelCommMonoidWithZero M] [UniqueFactorizationMonoid M]
+    [CommMonoidWithZero M] [IsCancelMulZero M] [UniqueFactorizationMonoid M]
     {a b : M} (ha : a ≠ 0) : a ∣ b ↔ ∀ p : M, Prime p → emultiplicity p a ≤ emultiplicity p b := by
   constructor
   · intro hab p _
@@ -52,8 +50,8 @@ lemma dvd_iff_emultiplicity_le {M : Type*}
           Nat.cast_le, add_comm, add_le_add_iff_left] at this
         exact le_emultiplicity_of_le_multiplicity this
 
-lemma pow_dvd_pow_iff_dvd {M : Type*} [CancelCommMonoidWithZero M] [UniqueFactorizationMonoid M]
-    {a b : M} {x : ℕ} (h' : x ≠ 0) : a ^ x ∣ b ^ x ↔ a ∣ b := by
+lemma pow_dvd_pow_iff_dvd {M : Type*} [CommMonoidWithZero M] [IsCancelMulZero M]
+    [UniqueFactorizationMonoid M] {a b : M} {x : ℕ} (h' : x ≠ 0) : a ^ x ∣ b ^ x ↔ a ∣ b := by
   classical
   by_cases ha : a = 0
   · simp [ha, h']
@@ -164,9 +162,6 @@ lemma exists_not_dvd_spanSingleton_eq {R : Type*} [CommRing R] [IsDomain R] [IsD
   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
-    refine hn (dvd_trans (pow_dvd_pow _ ?_) hs)
-    linarith
-  · intro ht
-    refine hm (dvd_trans (pow_dvd_pow _ (Nat.le_add_left _ _)) ht)
+  refine this (n + m + 1) (Nat.le_add_left 1 (n + m)) ⟨s, t, (fun hs ↦ ?_), (fun ht ↦ ?_), ha.symm⟩
+  · exact hn (dvd_trans (pow_dvd_pow _ (by linarith)) hs)
+  · exact hm (dvd_trans (pow_dvd_pow _ (Nat.le_add_left _ _)) ht)

FltRegular/NumberTheory/Hilbert92.lean

@@ -613,11 +613,6 @@ lemma relativeUnitsModule_zeta_smul (x) :
     LinearEquiv.symm_apply_apply, Module.End.smul_def, unit_to_U]
   rfl
 
-local instance {M} [AddCommGroup M] : NoZeroSMulDivisors ℤ (M ⧸ AddCommGroup.torsion M) := by
-  rw [← Submodule.torsion_int]
-  change NoZeroSMulDivisors ℤ (M ⧸ Submodule.torsion ℤ M)
-  infer_instance
-
 local instance : Module.Finite ℤ (Additive <| RelativeUnits k K) :=
   inferInstanceAs
     (Module.Finite ℤ (Additive (𝓞 K)ˣ ⧸ AddSubgroup.toIntSubmodule (Subgroup.toAddSubgroup
@@ -630,8 +625,6 @@ local instance : Module.Finite ℤ G := Module.Finite.of_surjective
   (M := Additive (relativeUnitsWithGenerator p hp hKL σ hσ))
   (QuotientAddGroup.mk' _).toIntLinearMap (QuotientAddGroup.mk'_surjective _)
 
-local instance : Module.Free ℤ G := Module.free_of_finite_type_torsion_free'
-
 noncomputable
 def unitlifts (S : systemOfUnits p G (NumberField.Units.rank k + 1)) :
     Fin (NumberField.Units.rank k + 1) → Additive (𝓞 K)ˣ :=

FltRegular/NumberTheory/Unramified.lean

@@ -38,11 +38,11 @@ class IsUnramified (R S : Type*) [CommRing R] [CommRing S] [Algebra R S] : Prop
 variable {R} {S}
 
 lemma prod_primesOverFinset_of_isUnramified [IsUnramified R S] [IsDedekindDomain S]
-    [NoZeroSMulDivisors R S] (p : Ideal R) [p.IsPrime] (hp : p ≠ ⊥) :
+    [Module.IsTorsionFree R S] (p : Ideal R) [p.IsPrime] (hp : p ≠ ⊥) :
     ∏ P ∈ primesOverFinset p S, P = p.map (algebraMap R S) := by
   classical
   have hpbot' : p.map (algebraMap R S) ≠ ⊥ := (Ideal.map_eq_bot_iff_of_injective
-    (NoZeroSMulDivisors.iff_algebraMap_injective.mp ‹_›)).not.mpr hp
+      (NoZeroSMulDivisors.iff_algebraMap_injective.mp inferInstance)).not.mpr hp
   rw [← associated_iff_eq.mp (factors_pow_count_prod hpbot')]
   apply Finset.prod_congr rfl
   intros P hP

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "cc1a61983e46cf9185c198e96f15542336dc2413",
+   "rev": "837f89af8e04d19de80221cb2b339049c998f7a4",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "53b324fd0c646e0b2d68cbaae666d40a02d20517",
+   "rev": "a720914be0e2cd39010bbc46d7736c8aeb209d2e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5ba0380f2fb45c69448d80429ef6c22bf5973cfa",
+   "rev": "c82094b2c4065eb1e3121a7e202cd8d7cc1bc66c",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",