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

Mathlib/Analysis/InnerProductSpace/MulOpposite.lean

@@ -26,31 +26,37 @@ 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
   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
 
+@[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 :