bump mathlib

ImperialCollegeLondon · Nov 9, 2024 · b35f4a7 · b35f4a7
1 parent c982409
commit b35f4a7
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 34 deletions.
diff --git a/FLT/NumberField/AdeleRing.lean b/FLT/NumberField/AdeleRing.lean
@@ -1,31 +1,7 @@
-import Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
-import Mathlib.NumberTheory.NumberField.Basic
+import Mathlib.NumberTheory.NumberField.AdeleRing
 
 universe u
 
-section PRed
--- Don't try anything in this section because we are missing a definition.
-
--- see mathlib PR #16485
-def NumberField.AdeleRing (K : Type u) [Field K] [NumberField K] : Type u := sorry
-
-open NumberField
-
-variable (K : Type*) [Field K] [NumberField K]
-
--- All these are already done in mathlib PRs, so can be assumed for now.
--- When they're in mathlib master we can update mathlib and then get these theorems/definitions
--- for free.
-instance : CommRing (AdeleRing K) := sorry
-
-instance : TopologicalSpace (AdeleRing K) := sorry
-
-instance : TopologicalRing (AdeleRing K) := sorry
-
-instance : Algebra K (AdeleRing K) := sorry
-
-end PRed
-
 section AdeleRingLocallyCompact
 -- This theorem is proved in another project, so we may as well assume it.
 
@@ -52,10 +28,3 @@ open NumberField
 theorem NumberField.AdeleRing.cocompact :
     CompactSpace (AdeleRing K ⧸ AddMonoidHom.range (algebraMap K (AdeleRing K)).toAddMonoidHom) :=
   sorry
-
--- Do we have this already?
-
--- Modulo everything above, and possibly also some other things, we can start working on
--- Main Theorem 27.6.14 of John Voight's quaternion algebra book
--- (https://jvoight.github.io/quat-book.pdf), p458 of the book,
--- which is p478 of the pdf.
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "61ccb312808a1e28bff528aa96811d45fc51ce0e",
+   "rev": "7fc8954db7c3e9619b2055e97afeda277df11e5a",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b6ae1cf11e83d972ffa363f9cdc8a2f89aaa24dc",
+   "rev": "e18c6c23dd7cb1f12d79d6304262351df943aa37",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",