[Merged by Bors] - chore(Analysis/InnerProductSpace/MulOpposite): NormedAddCommGroup -> SeminormedAddCommGroup

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,38 +25,53 @@ 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
   conj_inner_symm x y := InnerProductSpace.conj_inner_symm x.unop y.unop
   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
+@[simp] lemma _root_.OrthonormalBasis.toBasis_mulOpposite (b : OrthonormalBasis ι 𝕜 H) :
+    b.mulOpposite.toBasis = b.toBasis.mulOpposite := rfl
 
-variable (𝕜 H) in
+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 ≃ₗᵢ[𝕜] 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 opIsometry
 
 end MulOpposite