bump mathlib (#220)

ImperialCollegeLondon · Nov 17, 2024 · bbee48f · bbee48f
1 parent 24e02d3
commit bbee48f
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 13 deletions.
diff --git a/FLT/ForMathlib/MiscLemmas.lean b/FLT/ForMathlib/MiscLemmas.lean
@@ -69,6 +69,8 @@ variable {A : Type*} [SMul R A]
 variable {S : Type*} [τS : TopologicalSpace S] {f : S → R} (hf : Continuous f)
 variable {B : Type*} [SMul S B]
 
+open Topology
+
 -- note: use convert not exact to ensure typeclass inference doesn't try to find topology on B
 theorem induced_continuous_smul [τA : TopologicalSpace A] [ContinuousSMul R A] (g : B →ₑ[f] A)
     (hf : Continuous f) : @ContinuousSMul S B _ _ (TopologicalSpace.induced g τA) := by

diff --git a/FLT/MathlibExperiments/FrobeniusRiou.lean b/FLT/MathlibExperiments/FrobeniusRiou.lean
@@ -863,13 +863,13 @@ variable (L : Type*) [Field L] [Algebra (B ⧸ Q) L] [IsFractionRing (B ⧸ Q) L
 
 
 noncomputable def IsFractionRing.algEquiv_lift (e : (B ⧸ Q) ≃ₐ[A ⧸ P] B ⧸ Q) : L ≃ₐ[K] L where
-  __ := IsFractionRing.fieldEquivOfRingEquiv e.toRingEquiv
+  __ := IsFractionRing.ringEquivOfRingEquiv e.toRingEquiv
   commutes' := by
     intro k
     dsimp
-    obtain ⟨x, y, _, rfl⟩ := @IsFractionRing.div_surjective (A ⧸ P) _ _ K _ _ _ k
+    obtain ⟨x, y, _, rfl⟩ := @IsFractionRing.div_surjective (A ⧸ P) _ K _ _ _ k
     simp [algebraMap_algebraMap]
-    unfold IsFractionRing.fieldEquivOfRingEquiv
+    unfold IsFractionRing.ringEquivOfRingEquiv
     unfold IsLocalization.ringEquivOfRingEquiv
     simp [IsScalarTower.algebraMap_apply (A ⧸ P) (B ⧸ Q) L]
 
@@ -878,17 +878,17 @@ noncomputable def stabilizer.toGaloisGroup : MulAction.stabilizer G Q →* (L
   map_one' := by
     apply AlgEquiv.ext
     intro l; simp
-    obtain ⟨x, y, _, rfl⟩ := @IsFractionRing.div_surjective (B ⧸ Q) _ _ L _ _ _ l
+    obtain ⟨x, y, _, rfl⟩ := @IsFractionRing.div_surjective (B ⧸ Q) _ L _ _ _ l
     unfold IsFractionRing.algEquiv_lift
-    unfold IsFractionRing.fieldEquivOfRingEquiv
+    unfold IsFractionRing.ringEquivOfRingEquiv
     simp
   map_mul' := by
     intro ⟨x, hx⟩ ⟨y, hy⟩
     apply AlgEquiv.ext
     intro l; dsimp
-    obtain ⟨r, s, _, rfl⟩ := @IsFractionRing.div_surjective (B ⧸ Q) _ _ L _ _ _ l
+    obtain ⟨r, s, _, rfl⟩ := @IsFractionRing.div_surjective (B ⧸ Q) _ L _ _ _ l
     unfold IsFractionRing.algEquiv_lift
-    unfold IsFractionRing.fieldEquivOfRingEquiv
+    unfold IsFractionRing.ringEquivOfRingEquiv
     simp
     sorry
 

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "af731107d531b39cd7278c73f91c573f40340612",
+   "rev": "b100ff2565805e9f30a482788b3fc66937a7f38a",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5dfdc66e0d503631527ad90c1b5d7815c86a8662",
+   "rev": "de91b59101763419997026c35a41432ac8691f15",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ac7b989cbf99169509433124ae484318e953d201",
+   "rev": "b0b73e5bc33f1bc4d3c0f254630dd0e262cecc08",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "1964227ee4bc4a748a0fd3b7538fb3624bd53cdf",
+   "rev": "7b8edbb98887af54a4cb8e8f76fa279960233c22",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -115,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b41bc9cec7f433d6e1d74ff3b59edaaf58ad2915",
+   "rev": "2905ab4ec3961d1fd68ddae0ab4083497e579014",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e18c6c23dd7cb1f12d79d6304262351df943aa37",
+   "rev": "7b6a56e8e4fcf54d3834b225b9814a7c9e4d4bda",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",