chore(Analysis/InnerProductSpace/PiL2): Make EuclideanSpace.equiv an …

…`abbrev` (#6503)

This definition already exists elsewhere more generally, but this spelling is admittedly easier to find.

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 {ι 𝕜}