bump to nightly-2023-08-22-09

mathlib commit leanprover-community/mathlib@32a7e53

Mathbin/Analysis/NormedSpace/Star/Mul.lean

@@ -24,7 +24,6 @@ variable [DenselyNormedField 𝕜] [NonUnitalNormedRing E] [StarRing E] [CstarRi
 
 variable [NormedSpace 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] (a : E)
 
-#print op_nnnorm_mul /-
 /-- In a C⋆-algebra `E`, either unital or non-unital, multiplication on the left by `a : E` has
 norm equal to the norm of `a`. -/
 @[simp]
@@ -48,9 +47,7 @@ theorem op_nnnorm_mul : ‖mul 𝕜 E a‖₊ = ‖a‖₊ :=
     · simp only [map_smul, nnnorm_smul, mul_apply', mul_smul_comm, CstarRing.nnnorm_self_mul_star]
       rwa [← NNReal.div_lt_iff (mul_pos ha ha).ne', div_eq_mul_inv, mul_inv, ← mul_assoc]
 #align op_nnnorm_mul op_nnnorm_mul
--/
 
-#print op_nnnorm_mul_flip /-
 /-- In a C⋆-algebra `E`, either unital or non-unital, multiplication on the right by `a : E` has
 norm eqaul to the norm of `a`. -/
 @[simp]
@@ -64,23 +61,18 @@ theorem op_nnnorm_mul_flip : ‖(mul 𝕜 E).flip a‖₊ = ‖a‖₊ :=
   · simp only [← star_mul, nnnorm_star]
   · simpa using (nnnorm_star (star b * a)).symm
 #align op_nnnorm_mul_flip op_nnnorm_mul_flip
--/
 
 variable (E)
 
-#print mul_isometry /-
 /-- In a C⋆-algebra `E`, either unital or non-unital, the left regular representation is an
 isometry. -/
 theorem mul_isometry : Isometry (mul 𝕜 E) :=
   AddMonoidHomClass.isometry_of_norm _ fun a => congr_arg coe <| op_nnnorm_mul 𝕜 a
 #align mul_isometry mul_isometry
--/
 
-#print mul_flip_isometry /-
 /-- In a C⋆-algebra `E`, either unital or non-unital, the right regular anti-representation is an
 isometry. -/
 theorem mul_flip_isometry : Isometry (mul 𝕜 E).flip :=
   AddMonoidHomClass.isometry_of_norm _ fun a => congr_arg coe <| op_nnnorm_mul_flip 𝕜 a
 #align mul_flip_isometry mul_flip_isometry
--/
 

lake-manifest.json

@@ -12,10 +12,10 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "f5715d0739d7880c037f2e618f19af781e9e7679",
+    "rev": "6a8ee26e1d66f31273612f84567578bb72c5ef2e",
     "opts": {},
     "name": "lean3port",
-    "inputRev?": "f5715d0739d7880c037f2e618f19af781e9e7679",
+    "inputRev?": "6a8ee26e1d66f31273612f84567578bb72c5ef2e",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
@@ -28,10 +28,10 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "885480409e857a9bda3ca843d37ce9bfcd2c03d4",
+    "rev": "8f78230536025925db73016a9c366eebba2a5700",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "885480409e857a9bda3ca843d37ce9bfcd2c03d4",
+    "inputRev?": "8f78230536025925db73016a9c366eebba2a5700",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/gebner/quote4",

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-08-22-07"
+def tag : String := "nightly-2023-08-22-09"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"f5715d0739d7880c037f2e618f19af781e9e7679"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"6a8ee26e1d66f31273612f84567578bb72c5ef2e"
 
 @[default_target]
 lean_lib Mathbin where