bump to nightly-2023-03-19-18

mathlib commit leanprover-community/mathlib@1f4705c
leanprover-community · Mar 19, 2023 · a0aedb6 · a0aedb6
1 parent 8113930
commit a0aedb6
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 6 deletions.
diff --git a/Mathbin/Data/Zmod/Algebra.lean b/Mathbin/Data/Zmod/Algebra.lean
@@ -27,6 +27,7 @@ section
 
 variable {n : ℕ} (m : ℕ) [CharP R m]
 
+#print ZMod.algebra' /-
 /-- The `zmod n`-algebra structure on rings whose characteristic `m` divides `n` -/
 def algebra' (h : m ∣ n) : Algebra (ZMod n) R :=
   { ZMod.castHom h R with
@@ -40,6 +41,7 @@ def algebra' (h : m ∣ n) : Algebra (ZMod n) R :=
         exact Commute.cast_int_left r k
     smul_def' := fun a r => rfl }
 #align zmod.algebra' ZMod.algebra'
+-/
 
 end
 

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -4,15 +4,15 @@
  [{"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "e9f8c4b130145c0984e95a4e3ceaea90c87d87a5",
+    "rev": "7dd598f315c945d6a68b9c72e8f08f4d5205f840",
     "name": "lean3port",
-    "inputRev?": "e9f8c4b130145c0984e95a4e3ceaea90c87d87a5"}},
+    "inputRev?": "7dd598f315c945d6a68b9c72e8f08f4d5205f840"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "a86f11bb6623b0ffa089a4225f73ec406521c216",
+    "rev": "d8b38e198dd3ebe23cf93880a70f1ad0c17d2300",
     "name": "mathlib",
-    "inputRev?": "a86f11bb6623b0ffa089a4225f73ec406521c216"}},
+    "inputRev?": "d8b38e198dd3ebe23cf93880a70f1ad0c17d2300"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

diff --git a/lakefile.lean b/lakefile.lean
@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-03-19-16"
+def tag : String := "nightly-2023-03-19-18"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"e9f8c4b130145c0984e95a4e3ceaea90c87d87a5"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"7dd598f315c945d6a68b9c72e8f08f4d5205f840"
 
 @[default_target]
 lean_lib Mathbin where