From 263a28b66952aedcf79285340bc52e669492b896 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 11 Aug 2023 10:51:15 +0000 Subject: [PATCH] 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 | 17 +++++++---------- 1 file changed, 7 insertions(+), 10 deletions(-) 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 {ι 𝕜}