From e4323d02ba084a500e1040b09a4f5c5debc4cc1f Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Sun, 19 Oct 2025 13:47:55 +0000
Subject: [PATCH 01/10] seminormed

---
 .../InnerProductSpace/MulOpposite.lean        | 20 ++++++++++++-------
 1 file changed, 13 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
index 3f1bbb0ce56664..1d9383c072366e 100644
--- a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
+++ b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
@@ -26,7 +26,7 @@ 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]
+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,23 +34,29 @@ 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
 
+@[simp] lemma _root_.OrthonormalBasis.toBasis_mulOpposite (b : OrthonormalBasis ι 𝕜 H) :
+    b.mulOpposite.toBasis = b.toBasis.mulOpposite := rfl
+
+end orthonormal
+
 theorem isometry_opLinearEquiv {R M : Type*} [Semiring R] [SeminormedAddCommGroup M] [Module R M] :
-    Isometry (opLinearEquiv R (M:=M)) := fun _ _ => rfl
+    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
+def opLinearIsometryEquiv : H ≃ₗᵢ[𝕜] Hᵐᵒᵖ := (opLinearEquiv 𝕜).isometryOfInner inner_op
 
 @[simp]
 theorem toLinearEquiv_opLinearIsometryEquiv :

From 0041f62d0c159a64dffe24087cf532dab2c10e10 Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Sun, 19 Oct 2025 13:57:21 +0000
Subject: [PATCH 02/10] cleanup

---
 Mathlib/Analysis/InnerProductSpace/MulOpposite.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
index 1d9383c072366e..9ec0cba10621aa 100644
--- a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
+++ b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
@@ -35,12 +35,11 @@ instance : InnerProductSpace 𝕜 Hᵐᵒᵖ where
   smul_left x y r := InnerProductSpace.smul_left x.unop y.unop r
 
 section orthonormal
+variable {ι H : Type*} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [Fintype ι]
 
 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 (b : OrthonormalBasis ι 𝕜 H) :
     OrthonormalBasis ι 𝕜 Hᵐᵒᵖ := b.toBasis.mulOpposite.toOrthonormalBasis b.orthonormal

From 785bf17d6c4ae8d44f6ab20f21bf3d441392368c Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Sun, 19 Oct 2025 13:58:00 +0000
Subject: [PATCH 03/10] revert

---
 Mathlib/Analysis/InnerProductSpace/MulOpposite.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
index 9ec0cba10621aa..1d9383c072366e 100644
--- a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
+++ b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
@@ -35,11 +35,12 @@ instance : InnerProductSpace 𝕜 Hᵐᵒᵖ where
   smul_left x y r := InnerProductSpace.smul_left x.unop y.unop r
 
 section orthonormal
-variable {ι H : Type*} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [Fintype ι]
 
 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 (b : OrthonormalBasis ι 𝕜 H) :
     OrthonormalBasis ι 𝕜 Hᵐᵒᵖ := b.toBasis.mulOpposite.toOrthonormalBasis b.orthonormal

From 9d6418e278f8200ce989abafe75e8119091694e6 Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Sun, 19 Oct 2025 21:23:32 +0000
Subject: [PATCH 04/10] generalize

---
 Mathlib/Analysis/InnerProductSpace/MulOpposite.lean | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
index 1d9383c072366e..654fb46f913e91 100644
--- a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
+++ b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
@@ -26,7 +26,10 @@ 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 𝕜] [SeminormedAddCommGroup H] [InnerProductSpace 𝕜 H]
+variable [SeminormedAddCommGroup H]
+
+section InnerProductSpace
+variable [RCLike 𝕜] [InnerProductSpace 𝕜 H]
 
 instance : InnerProductSpace 𝕜 Hᵐᵒᵖ where
   norm_sq_eq_re_inner x := (inner_self_eq_norm_sq x.unop).symm
@@ -49,14 +52,19 @@ noncomputable def _root_.OrthonormalBasis.mulOpposite (b : OrthonormalBasis ι 
     b.mulOpposite.toBasis = b.toBasis.mulOpposite := rfl
 
 end orthonormal
+end InnerProductSpace
 
 theorem isometry_opLinearEquiv {R M : Type*} [Semiring R] [SeminormedAddCommGroup M] [Module R M] :
     Isometry (opLinearEquiv R (M := M)) := fun _ _ => rfl
 
+variable [NormedField 𝕜] [NormedSpace 𝕜 H]
+
 variable (𝕜 H) in
 /-- The linear isometry equivalence version of the function `op`. -/
 @[simps!]
-def opLinearIsometryEquiv : H ≃ₗᵢ[𝕜] Hᵐᵒᵖ := (opLinearEquiv 𝕜).isometryOfInner inner_op
+def opLinearIsometryEquiv : H ≃ₗᵢ[𝕜] Hᵐᵒᵖ where
+  toLinearEquiv := opLinearEquiv 𝕜
+  norm_map' _ := rfl
 
 @[simp]
 theorem toLinearEquiv_opLinearIsometryEquiv :

From 6f4b268e28c4afd05a3d1c1a9aaf233c4648d480 Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Sun, 19 Oct 2025 21:28:08 +0000
Subject: [PATCH 05/10] generalize further

---
 .../Analysis/InnerProductSpace/MulOpposite.lean    | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
index 654fb46f913e91..b1c50b838371df 100644
--- a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
+++ b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
@@ -13,7 +13,7 @@ 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*}
+variable {R 𝕜 H : Type*}
 
 namespace MulOpposite
 
@@ -57,21 +57,21 @@ end InnerProductSpace
 theorem isometry_opLinearEquiv {R M : Type*} [Semiring R] [SeminormedAddCommGroup M] [Module R M] :
     Isometry (opLinearEquiv R (M := M)) := fun _ _ => rfl
 
-variable [NormedField 𝕜] [NormedSpace 𝕜 H]
+variable [Semiring R] [Module R H]
 
-variable (𝕜 H) in
+variable (R H) in
 /-- The linear isometry equivalence version of the function `op`. -/
 @[simps!]
-def opLinearIsometryEquiv : H ≃ₗᵢ[𝕜] Hᵐᵒᵖ where
-  toLinearEquiv := opLinearEquiv 𝕜
+def opLinearIsometryEquiv : H ≃ₗᵢ[R] Hᵐᵒᵖ where
+  toLinearEquiv := opLinearEquiv R
   norm_map' _ := rfl
 
 @[simp]
 theorem toLinearEquiv_opLinearIsometryEquiv :
-    (opLinearIsometryEquiv 𝕜 H).toLinearEquiv = opLinearEquiv 𝕜 := rfl
+    (opLinearIsometryEquiv R H).toLinearEquiv = opLinearEquiv R := rfl
 
 @[simp]
 theorem toContinuousLinearEquiv_opLinearIsometryEquiv :
-    (opLinearIsometryEquiv 𝕜 H).toContinuousLinearEquiv = opContinuousLinearEquiv 𝕜 := rfl
+    (opLinearIsometryEquiv R H).toContinuousLinearEquiv = opContinuousLinearEquiv R := rfl
 
 end MulOpposite

From fcc59ab4242cd2d609c97d3e32f2566bcb974d66 Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Sun, 19 Oct 2025 21:31:52 +0000
Subject: [PATCH 06/10] cleanup

---
 Mathlib/Analysis/InnerProductSpace/MulOpposite.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
index b1c50b838371df..3cdcb77f073516 100644
--- a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
+++ b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
@@ -54,11 +54,10 @@ noncomputable def _root_.OrthonormalBasis.mulOpposite (b : OrthonormalBasis ι 
 end orthonormal
 end InnerProductSpace
 
-theorem isometry_opLinearEquiv {R M : Type*} [Semiring R] [SeminormedAddCommGroup M] [Module R M] :
-    Isometry (opLinearEquiv R (M := M)) := fun _ _ => rfl
-
 variable [Semiring R] [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!]

From 46b873d7298cc6ab8b332f93f7469f39d4d7b4d9 Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Sun, 19 Oct 2025 21:42:40 +0000
Subject: [PATCH 07/10] variables

---
 Mathlib/Analysis/InnerProductSpace/MulOpposite.lean | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
index 3cdcb77f073516..a437c1062b0a6b 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 {R 𝕜 H : Type*}
-
 namespace MulOpposite
+variable {𝕜 H : Type*}
 
 open MulOpposite
 
@@ -26,10 +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 [SeminormedAddCommGroup H]
-
 section InnerProductSpace
-variable [RCLike 𝕜] [InnerProductSpace 𝕜 H]
+variable [RCLike 𝕜] [SeminormedAddCommGroup H] [InnerProductSpace 𝕜 H]
 
 instance : InnerProductSpace 𝕜 Hᵐᵒᵖ where
   norm_sq_eq_re_inner x := (inner_self_eq_norm_sq x.unop).symm
@@ -54,7 +51,7 @@ noncomputable def _root_.OrthonormalBasis.mulOpposite (b : OrthonormalBasis ι 
 end orthonormal
 end InnerProductSpace
 
-variable [Semiring R] [Module R H]
+variable {R H : Type*} [SeminormedAddCommGroup H] [Semiring R] [Module R H]
 
 theorem isometry_opLinearEquiv : Isometry (opLinearEquiv R (M := H)) := fun _ _ => rfl
 

From d1e584adb705ea3dbfa226bbcbb678d9b2db069a Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Sun, 19 Oct 2025 21:43:05 +0000
Subject: [PATCH 08/10] reorder

---
 Mathlib/Analysis/InnerProductSpace/MulOpposite.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
index a437c1062b0a6b..0ff2698ddb108c 100644
--- a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
+++ b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
@@ -51,7 +51,7 @@ noncomputable def _root_.OrthonormalBasis.mulOpposite (b : OrthonormalBasis ι 
 end orthonormal
 end InnerProductSpace
 
-variable {R H : Type*} [SeminormedAddCommGroup H] [Semiring R] [Module R H]
+variable {R H : Type*} [Semiring R] [SeminormedAddCommGroup H] [Module R H]
 
 theorem isometry_opLinearEquiv : Isometry (opLinearEquiv R (M := H)) := fun _ _ => rfl
 

From cdad49e907cfb28d67ab1c1d62d07e3b674872ef Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Sun, 19 Oct 2025 21:45:04 +0000
Subject: [PATCH 09/10] section

---
 Mathlib/Analysis/InnerProductSpace/MulOpposite.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
index 0ff2698ddb108c..82478fb5126cb9 100644
--- a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
+++ b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
@@ -49,8 +49,10 @@ noncomputable def _root_.OrthonormalBasis.mulOpposite (b : OrthonormalBasis ι 
     b.mulOpposite.toBasis = b.toBasis.mulOpposite := rfl
 
 end orthonormal
+
 end InnerProductSpace
 
+section opIsometry
 variable {R H : Type*} [Semiring R] [SeminormedAddCommGroup H] [Module R H]
 
 theorem isometry_opLinearEquiv : Isometry (opLinearEquiv R (M := H)) := fun _ _ => rfl
@@ -70,4 +72,6 @@ theorem toLinearEquiv_opLinearIsometryEquiv :
 theorem toContinuousLinearEquiv_opLinearIsometryEquiv :
     (opLinearIsometryEquiv R H).toContinuousLinearEquiv = opContinuousLinearEquiv R := rfl
 
+end opIsometry
+
 end MulOpposite

From 1dba9ba1110d363bf1fee3192ef0e27d268f1bab Mon Sep 17 00:00:00 2001
From: Monica Omar <2497250a@research.gla.ac.uk>
Date: Mon, 20 Oct 2025 03:43:36 +0000
Subject: [PATCH 10/10] move section

---
 .../InnerProductSpace/MulOpposite.lean        | 22 -------------------
 .../Normed/Operator/LinearIsometry.lean       | 22 +++++++++++++++++++
 2 files changed, 22 insertions(+), 22 deletions(-)

diff --git a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
index 82478fb5126cb9..51886b80c43ffb 100644
--- a/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
+++ b/Mathlib/Analysis/InnerProductSpace/MulOpposite.lean
@@ -52,26 +52,4 @@ end orthonormal
 
 end InnerProductSpace
 
-section opIsometry
-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 opIsometry
-
 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