bump to nightly-2023-03-20-10

mathlib commit leanprover-community/mathlib@7ec2946
leanprover-community · Mar 20, 2023 · 0469e46 · 0469e46
1 parent 2396028
commit 0469e46
Show file tree

Hide file tree

Showing 4 changed files with 38 additions and 20 deletions.
diff --git a/Mathbin/Algebra/DirectSum/Finsupp.lean b/Mathbin/Algebra/DirectSum/Finsupp.lean
diff --git a/Mathbin/LinearAlgebra/DirectSum/Finsupp.lean b/Mathbin/LinearAlgebra/DirectSum/Finsupp.lean
@@ -39,9 +39,9 @@ open TensorProduct Classical
 /-- The tensor product of ι →₀ M and κ →₀ N is linearly equivalent to (ι × κ) →₀ (M ⊗ N). -/
 def finsuppTensorFinsupp (R M N ι κ : Sort _) [CommRing R] [AddCommGroup M] [Module R M]
     [AddCommGroup N] [Module R N] : (ι →₀ M) ⊗[R] (κ →₀ N) ≃ₗ[R] ι × κ →₀ M ⊗[R] N :=
-  TensorProduct.congr (finsuppLequivDirectSum R M ι) (finsuppLequivDirectSum R N κ) ≪≫ₗ
+  TensorProduct.congr (finsuppLEquivDirectSum R M ι) (finsuppLEquivDirectSum R N κ) ≪≫ₗ
     ((TensorProduct.directSum R (fun _ : ι => M) fun _ : κ => N) ≪≫ₗ
-      (finsuppLequivDirectSum R (M ⊗[R] N) (ι × κ)).symm)
+      (finsuppLEquivDirectSum R (M ⊗[R] N) (ι × κ)).symm)
 #align finsupp_tensor_finsupp finsuppTensorFinsupp
 
 @[simp]

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": "693bed9121b174d067f8a4a8e35df5b602200a37",
+    "rev": "d34a07f2a36e4671efb78f17dd1ab012f111f008",
     "name": "lean3port",
-    "inputRev?": "693bed9121b174d067f8a4a8e35df5b602200a37"}},
+    "inputRev?": "d34a07f2a36e4671efb78f17dd1ab012f111f008"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "e3cd24829ee170492d251da5878e7dc98e52479b",
+    "rev": "7307cd34049d6ba8b5901766daabe441a8fcc08c",
     "name": "mathlib",
-    "inputRev?": "e3cd24829ee170492d251da5878e7dc98e52479b"}},
+    "inputRev?": "7307cd34049d6ba8b5901766daabe441a8fcc08c"}},
   {"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-20-08"
+def tag : String := "nightly-2023-03-20-10"
 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"@"693bed9121b174d067f8a4a8e35df5b602200a37"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"d34a07f2a36e4671efb78f17dd1ab012f111f008"
 
 @[default_target]
 lean_lib Mathbin where