bump

leanprover-community · Nov 13, 2024 · 59c9644 · 59c9644
1 parent 939f8f2
commit 59c9644
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 10 deletions.
diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean
@@ -9,7 +9,6 @@ import Mathlib.RingTheory.Henselian
 import Mathlib.LinearAlgebra.Dimension.Torsion
 import Mathlib.GroupTheory.FiniteAbelian.Basic
 
-
 open scoped NumberField nonZeroDivisors
 open FiniteDimensional NumberField
 
@@ -329,7 +328,7 @@ lemma isTors' [IsGalois k K] : Module.IsTorsionBySet ℤ[X]
   obtain ⟨x, rfl⟩ := Additive.ofMul.surjective x
   obtain ⟨x, rfl⟩ := QuotientGroup.mk_surjective x
   rw [← Module.AEval.of_aeval_smul]
-  simp_rw [LinearMap.smul_def, Polynomial.cyclotomic_prime ℤ p, AddEquivClass.map_eq_zero_iff,
+  simp_rw [LinearMap.smul_def, Polynomial.cyclotomic_prime ℤ p, EmbeddingLike.map_eq_zero_iff,
     map_sum, map_pow, aeval_X, LinearMap.coeFn_sum, sum_apply, ← relativeUnitsMapHom_apply,
     ← map_pow, ← Units.val_pow_eq_pow_val, ← map_pow, AlgEquiv.val_algHomUnitsEquiv_symm_apply,
     relativeUnitsMapHom_apply, Monoid.EndAdditive_apply,

diff --git a/FltRegular/NumberTheory/IdealNorm.lean b/FltRegular/NumberTheory/IdealNorm.lean
@@ -219,11 +219,11 @@ lemma NoZeroSMulDivisors_of_isLocalization (R S Rₚ Sₚ) [CommRing R] [CommRin
 theorem IsLocalization.AtPrime.PID_of_dedekind_domain {A} [CommRing A]
     [IsDedekindDomain A]
     (P : Ideal A) [pP : P.IsPrime] (Aₘ : Type*) [CommRing Aₘ] [IsDomain Aₘ]
-    [Algebra A Aₘ] [IsLocalization.AtPrime Aₘ P] : IsPrincipalIdealRing Aₘ := by
-  letI : IsNoetherianRing Aₘ :=
+    [Algebra A Aₘ] [IsLocalization.AtPrime Aₘ P] : IsPrincipalIdealRing Aₘ :=
+  have : IsNoetherianRing Aₘ :=
     IsLocalization.isNoetherianRing P.primeCompl _ IsDedekindRing.toIsNoetherian
-  letI : LocalRing Aₘ := IsLocalization.AtPrime.localRing Aₘ P
-  exact ((tfae_of_isNoetherianRing_of_localRing_of_isDomain Aₘ).out 2 0).mp
+  have : IsLocalRing Aₘ := IsLocalization.AtPrime.isLocalRing Aₘ P
+  ((tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain Aₘ).out 2 0).mp
     (IsLocalization.AtPrime.isDedekindDomain A P _)
 
 end

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "44f2360f50d0d3aea24653103a3f11ef5de9eb90",
+   "rev": "11da075dd931360a652129305eb045e5b1126ffd",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5dfdc66e0d503631527ad90c1b5d7815c86a8662",
+   "rev": "39119d25ce6f40a6250b742c6b4e8d9b400af677",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "94c3588e7610655b02f3203d3ef920730c45a2e2",
+   "rev": "3597f15bb5cd3e841064f98286c5549b22818a99",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6e6a825641f66cbb5ed12bc0e8513e9768e1ff0a",
+   "rev": "3a296bbf01538edd592ca5bbdec389768d6abed4",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",