bump

leanprover-community · Feb 13, 2025 · c2bbb3b · c2bbb3b
1 parent 7d7ef20
commit c2bbb3b
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 14 deletions.
diff --git a/FltRegular/NumberTheory/Unramified.lean b/FltRegular/NumberTheory/Unramified.lean
@@ -20,7 +20,7 @@ import Mathlib.NumberTheory.RamificationInertia.Basic
   is separable for some ideal `p` of `R` (with `f` being the minpoly of `α` over `R`), then `S/R` is
   unramified at `p`.
 -/
-open BigOperators UniqueFactorizationMonoid
+open BigOperators UniqueFactorizationMonoid Ideal
 
 attribute [local instance] FractionRing.liftAlgebra
 
@@ -150,8 +150,8 @@ lemma isUnramifiedAt_of_Separable_minpoly' [Algebra.IsSeparable K L]
   have := IsIntegralClosure.isFractionRing_of_finite_extension R K L S
   have := aeval_derivative_mem_differentIdeal R K L x hx'
   have H : RingHom.comp (algebraMap (FractionRing R) (FractionRing S))
-    ↑(FractionRing.algEquiv R K).symm.toRingEquiv =
-      RingHom.comp ↑(FractionRing.algEquiv S L).symm.toRingEquiv (algebraMap K L) := by
+    (FractionRing.algEquiv R K).symm.toRingEquiv =
+      RingHom.comp (FractionRing.algEquiv S L).symm.toRingEquiv (algebraMap K L) := by
     apply IsLocalization.ringHom_ext R⁰
     ext
     simp only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_comp, RingHom.coe_coe,
@@ -177,12 +177,12 @@ lemma isUnramifiedAt_of_Separable_minpoly' [Algebra.IsSeparable K L]
     have := hP.2.1
     rw [Ideal.under_def] at this
     have := (separable_map (Ideal.quotientMap P (algebraMap R S) this.symm.ge)).mpr h
-    rw [map_map, Ideal.quotientMap_comp_mk] at this
+    rw [Polynomial.map_map, Ideal.quotientMap_comp_mk] at this
     obtain ⟨a, b, e⟩ := this
     apply_fun (aeval (Ideal.Quotient.mk P x)) at e
-    simp_rw [← Ideal.Quotient.algebraMap_eq, ← map_map, derivative_map, map_add, map_mul,
-      aeval_map_algebraMap, aeval_algebraMap_apply, minpoly.aeval, hxP, map_zero, mul_zero,
-      zero_add, map_one, zero_ne_one] at e
+    simp_rw [← Ideal.Quotient.algebraMap_eq, ← Polynomial.map_map, derivative_map, map_add,
+      _root_.map_mul, aeval_map_algebraMap, aeval_algebraMap_apply, minpoly.aeval, hxP, map_zero,
+      mul_zero, zero_add, map_one, zero_ne_one] at e
   · rwa [Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count _
       (isMaximal_of_mem_primesOver hpbot hP).isPrime (ne_bot_of_mem_primesOver hpbot hP),
       Multiset.one_le_count_iff_mem, ← Multiset.mem_toFinset, ← primesOverFinset,

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f4d724054cac3c910ff00390b21dbe0f7105edac",
+   "rev": "e3f8a871d2beb4264e31eee6e3e4ee504b88638f",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "415af18dac1c4cb944eded206575c5b3422a9f2e",
+   "rev": "2278a5425c3783508a03bd72a9f9ff0b65d4c6e0",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531",
+   "rev": "0c169a0d55fef3763cfb3099eafd7b884ec7e41d",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5013810061a18ca1f5510106172b94c6fbd0a2fc",
+   "rev": "461b96f5527089718cb23d3f1fd2960a5d0ff516",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,10 +105,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8fff3f074da9237cd4e179fd6dd89be6c4022d41",
+   "rev": "322a050322e97b0a701588d9b1efbe2bee7f8527",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v0.0.52-pre2",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "512d7fa38234139a34c04e3b3438fc142b51bbee",
+   "rev": "b18855cb0f9a19bd4d7e21f3e5525272e377f431",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",