bump to nightly-2023-05-02-10

mathlib commit leanprover-community/mathlib@3947876
leanprover-community · May 2, 2023 · 951bc42 · 951bc42
1 parent 5a328b2
commit 951bc42
Show file tree

Hide file tree

Showing 7 changed files with 401 additions and 111 deletions.
diff --git a/Mathbin/Analysis/NormedSpace/Star/Spectrum.lean b/Mathbin/Analysis/NormedSpace/Star/Spectrum.lean
@@ -193,7 +193,7 @@ noncomputable instance (priority := 100) : StarHomClass F A ℂ
   coe_injective' := FunLike.coe_injective'
   map_star φ a := by
     suffices hsa : ∀ s : selfAdjoint A, (φ s)⋆ = φ s
-    · rw [← realPart_add_i_smul_imaginaryPart a]
+    · rw [← realPart_add_I_smul_imaginaryPart a]
       simp only [map_add, map_smul, star_add, star_smul, hsa, selfAdjoint.star_val_eq]
     · intro s
       have := AlgHom.apply_mem_spectrum φ (s : A)

diff --git a/Mathbin/Data/Complex/Basic.lean b/Mathbin/Data/Complex/Basic.lean
diff --git a/Mathbin/Data/Complex/Exponential.lean b/Mathbin/Data/Complex/Exponential.lean
diff --git a/Mathbin/Data/Complex/Module.lean b/Mathbin/Data/Complex/Module.lean
diff --git a/Mathbin/LinearAlgebra/CliffordAlgebra/Equivs.lean b/Mathbin/LinearAlgebra/CliffordAlgebra/Equivs.lean
@@ -183,7 +183,7 @@ def ofComplex : ℂ →ₐ[ℝ] CliffordAlgebra q :=
 
 @[simp]
 theorem ofComplex_i : ofComplex Complex.I = ι q 1 :=
-  Complex.liftAux_apply_i _ _
+  Complex.liftAux_apply_I _ _
 #align clifford_algebra_complex.of_complex_I CliffordAlgebraComplex.ofComplex_i
 
 @[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": "27674d71f2e3c650c886f678ec5e558abcd9a080",
+    "rev": "e45c4605d7b93cc5ed7d9c1e3312c5afe0d5020a",
     "name": "lean3port",
-    "inputRev?": "27674d71f2e3c650c886f678ec5e558abcd9a080"}},
+    "inputRev?": "e45c4605d7b93cc5ed7d9c1e3312c5afe0d5020a"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "d5f2c21d880775b1d309336bce5c58977751fb48",
+    "rev": "685bd4da4194abb102b827da14eac25c34d18c5f",
     "name": "mathlib",
-    "inputRev?": "d5f2c21d880775b1d309336bce5c58977751fb48"}},
+    "inputRev?": "685bd4da4194abb102b827da14eac25c34d18c5f"}},
   {"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-05-02-08"
+def tag : String := "nightly-2023-05-02-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"@"27674d71f2e3c650c886f678ec5e558abcd9a080"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"e45c4605d7b93cc5ed7d9c1e3312c5afe0d5020a"
 
 @[default_target]
 lean_lib Mathbin where