bump to nightly-2023-05-21-11

mathlib commit leanprover-community/mathlib@33c67ae
leanprover-community · May 21, 2023 · edafec7 · edafec7
1 parent 6b18fd9
commit edafec7
Show file tree

Hide file tree

Showing 5 changed files with 172 additions and 6 deletions.
diff --git a/Mathbin/Analysis/NormedSpace/Star/Basic.lean b/Mathbin/Analysis/NormedSpace/Star/Basic.lean
@@ -474,11 +474,13 @@ theorem starₗᵢ_apply {x : E} : starₗᵢ 𝕜 x = star x :=
   rfl
 #align starₗᵢ_apply starₗᵢ_apply
 
+#print starₗᵢ_toContinuousLinearEquiv /-
 @[simp]
 theorem starₗᵢ_toContinuousLinearEquiv :
     (starₗᵢ 𝕜 : E ≃ₗᵢ⋆[𝕜] E).toContinuousLinearEquiv = (starL 𝕜 : E ≃L⋆[𝕜] E) :=
   ContinuousLinearEquiv.ext rfl
 #align starₗᵢ_to_continuous_linear_equiv starₗᵢ_toContinuousLinearEquiv
+-/
 
 end starₗᵢ
 

diff --git a/Mathbin/Analysis/NormedSpace/Star/Mul.lean b/Mathbin/Analysis/NormedSpace/Star/Mul.lean