fix docstring

EtienneC30 · EtienneC30 · commit dc52315cc483 · 2026-03-16T11:07:15.000+01:00
diff --git a/Mathlib/Analysis/InnerProductSpace/PiL2.lean b/Mathlib/Analysis/InnerProductSpace/PiL2.lean
@@ -216,7 +216,7 @@ section restrict₂
 
 variable {I J : Finset ι'}
 
-/-- The restriction from `EuclideanSpace 𝕜 J` to `EuclideanSpace κ I` when `I ⊆ J`. -/
+/-- The restriction from `EuclideanSpace 𝕜 J` to `EuclideanSpace 𝕜 I` when `I ⊆ J`. -/
 noncomputable
 def restrict₂ (hIJ : I ⊆ J) :
     EuclideanSpace 𝕜 J →L[𝕜] EuclideanSpace 𝕜 I where
