diff --git a/Mathlib/Analysis/InnerProductSpace/PiL2.lean b/Mathlib/Analysis/InnerProductSpace/PiL2.lean
index 88942176928e6..01f42aa2fe4f8 100644
--- a/Mathlib/Analysis/InnerProductSpace/PiL2.lean
+++ b/Mathlib/Analysis/InnerProductSpace/PiL2.lean
@@ -212,17 +212,14 @@ end
 
 variable (ι 𝕜)
 
--- TODO : This should be generalized to `PiLp` with finite dimensional factors.
-/-- `PiLp.linearEquiv` upgraded to a continuous linear map between `EuclideanSpace 𝕜 ι`
-and `ι → 𝕜`. -/
-@[simps! toLinearEquiv_apply apply toLinearEquiv_symm_apply symm_apply]
-def EuclideanSpace.equiv : EuclideanSpace 𝕜 ι ≃L[𝕜] ι → 𝕜 :=
-  (PiLp.linearEquiv 2 𝕜 fun _ : ι => 𝕜).toContinuousLinearEquiv
+/-- A shorthand for `PiLp.continuousLinearEquiv`. -/
+abbrev EuclideanSpace.equiv : EuclideanSpace 𝕜 ι ≃L[𝕜] ι → 𝕜 :=
+  PiLp.continuousLinearEquiv 2 𝕜 _
 #align euclidean_space.equiv EuclideanSpace.equiv
-#align euclidean_space.equiv_to_linear_equiv_apply EuclideanSpace.equiv_toLinearEquiv_apply
-#align euclidean_space.equiv_apply EuclideanSpace.equiv_apply
-#align euclidean_space.equiv_to_linear_equiv_symm_apply EuclideanSpace.equiv_toLinearEquiv_symm_apply
-#align euclidean_space.equiv_symm_apply EuclideanSpace.equiv_symm_apply
+#noalign euclidean_space.equiv_to_linear_equiv_apply
+#noalign euclidean_space.equiv_apply
+#noalign euclidean_space.equiv_to_linear_equiv_symm_apply
+#noalign euclidean_space.equiv_symm_apply
 
 variable {ι 𝕜}