diff --git a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
index 3f1bbb0ce56664..51886b80c43ffb 100644
--- a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
+++ b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
@@ -13,9 +13,8 @@ This file defines the inner product space structure on `Hᵐᵒᵖ` where we def
 the inner product naturally. We also define `OrthonormalBasis.mulOpposite`.
 -/
 
-variable {𝕜 H : Type*}
-
 namespace MulOpposite
+variable {𝕜 H : Type*}
 
 open MulOpposite
 
@@ -26,7 +25,8 @@ instance [Inner 𝕜 H] : Inner 𝕜 Hᵐᵒᵖ where inner x y := inner 𝕜 x.
 
 @[simp] theorem inner_op [Inner 𝕜 H] (x y : H) : inner 𝕜 (op x) (op y) = inner 𝕜 x y := rfl
 
-variable [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H]
+section InnerProductSpace
+variable [RCLike 𝕜] [SeminormedAddCommGroup H] [InnerProductSpace 𝕜 H]
 
 instance : InnerProductSpace 𝕜 Hᵐᵒᵖ where
   norm_sq_eq_re_inner x := (inner_self_eq_norm_sq x.unop).symm
@@ -34,30 +34,22 @@ instance : InnerProductSpace 𝕜 Hᵐᵒᵖ where
   add_left x y z := InnerProductSpace.add_left x.unop y.unop z.unop
   smul_left x y r := InnerProductSpace.smul_left x.unop y.unop r
 
+section orthonormal
+
 theorem _root_.Module.Basis.mulOpposite_is_orthonormal_iff {ι : Type*} (b : Module.Basis ι 𝕜 H) :
     Orthonormal 𝕜 b.mulOpposite ↔ Orthonormal 𝕜 b := Iff.rfl
 
+variable {ι H : Type*} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [Fintype ι]
+
 /-- The multiplicative opposite of an orthonormal basis `b`, i.e., `b i ↦ op (b i)`. -/
-noncomputable def _root_.OrthonormalBasis.mulOpposite {ι : Type*}
-    [Fintype ι] (b : OrthonormalBasis ι 𝕜 H) :
+noncomputable def _root_.OrthonormalBasis.mulOpposite (b : OrthonormalBasis ι 𝕜 H) :
     OrthonormalBasis ι 𝕜 Hᵐᵒᵖ := b.toBasis.mulOpposite.toOrthonormalBasis b.orthonormal
 
-theorem isometry_opLinearEquiv {R M : Type*} [Semiring R] [SeminormedAddCommGroup M] [Module R M] :
-    Isometry (opLinearEquiv R (M:=M)) := fun _ _ => rfl
-
-variable (𝕜 H) in
-/-- The linear isometry equivalence version of the function `op`. -/
-@[simps!]
-def opLinearIsometryEquiv : H ≃ₗᵢ[𝕜] Hᵐᵒᵖ where
-  toLinearEquiv := opLinearEquiv 𝕜
-  norm_map' _ := rfl
+@[simp] lemma _root_.OrthonormalBasis.toBasis_mulOpposite (b : OrthonormalBasis ι 𝕜 H) :
+    b.mulOpposite.toBasis = b.toBasis.mulOpposite := rfl
 
-@[simp]
-theorem toLinearEquiv_opLinearIsometryEquiv :
-    (opLinearIsometryEquiv 𝕜 H).toLinearEquiv = opLinearEquiv 𝕜 := rfl
+end orthonormal
 
-@[simp]
-theorem toContinuousLinearEquiv_opLinearIsometryEquiv :
-    (opLinearIsometryEquiv 𝕜 H).toContinuousLinearEquiv = opContinuousLinearEquiv 𝕜 := rfl
+end InnerProductSpace
 
 end MulOpposite
diff --git a/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean b/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean
index 1914f7184d71ef..d545f2fdb553d5 100644
--- a/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean
+++ b/Mathlib/Analysis/Normed/Operator/LinearIsometry.lean
@@ -1070,3 +1070,25 @@ noncomputable def LinearIsometry.equivRange {R S : Type*} [Semiring R] [Ring S]
     [Module R F] {σ₁₂ : R →+* S} {σ₂₁ : S →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂]
     (f : F →ₛₗᵢ[σ₁₂] E) : F ≃ₛₗᵢ[σ₁₂] (LinearMap.range f.toLinearMap) :=
   { f with toLinearEquiv := LinearEquiv.ofInjective f.toLinearMap f.injective }
+
+namespace MulOpposite
+variable {R H : Type*} [Semiring R] [SeminormedAddCommGroup H] [Module R H]
+
+theorem isometry_opLinearEquiv : Isometry (opLinearEquiv R (M := H)) := fun _ _ => rfl
+
+variable (R H) in
+/-- The linear isometry equivalence version of the function `op`. -/
+@[simps!]
+def opLinearIsometryEquiv : H ≃ₗᵢ[R] Hᵐᵒᵖ where
+  toLinearEquiv := opLinearEquiv R
+  norm_map' _ := rfl
+
+@[simp]
+theorem toLinearEquiv_opLinearIsometryEquiv :
+    (opLinearIsometryEquiv R H).toLinearEquiv = opLinearEquiv R := rfl
+
+@[simp]
+theorem toContinuousLinearEquiv_opLinearIsometryEquiv :
+    (opLinearIsometryEquiv R H).toContinuousLinearEquiv = opContinuousLinearEquiv R := rfl
+
+end MulOpposite