few updates

Monlib/LinearAlgebra/InnerAut.lean

@@ -10,7 +10,7 @@ import Monlib.LinearAlgebra.MyMatrix.PosEqLinearMapIsPositive
 import Monlib.LinearAlgebra.MyTensorProduct
 import Monlib.RepTheory.AutMat
 import Monlib.Preq.StarAlgEquiv
-import Mathlib.Tactic.Explode
+-- import Mathlib.Tactic.Explode
 
 #align_import linear_algebra.innerAut
 

Monlib/LinearAlgebra/IsProj'.lean

@@ -39,7 +39,7 @@ end
 
 variable {E 𝕜 : Type _} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
 
-theorem orthogonalProjection_eq_linear_proj' {K : Submodule 𝕜 E} [CompleteSpace K] :
+theorem orthogonalProjection_eq_linear_proj' {K : Submodule 𝕜 E} [HasOrthogonalProjection K] :
     (orthogonalProjection K : E →ₗ[𝕜] K) =
       Submodule.linearProjOfIsCompl K _ Submodule.isCompl_orthogonal_of_completeSpace :=
   by
@@ -49,15 +49,15 @@ theorem orthogonalProjection_eq_linear_proj' {K : Submodule 𝕜 E} [CompleteSpa
   rw [ContinuousLinearMap.coe_coe, map_add, orthogonalProjection_mem_subspace_eq_self,
     orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero (Submodule.coe_mem _), add_zero]
 
-theorem orthogonalProjection_eq_linear_proj'' {K : Submodule 𝕜 E} [CompleteSpace K] (x : E) :
+theorem orthogonalProjection_eq_linear_proj'' {K : Submodule 𝕜 E} [HasOrthogonalProjection K] (x : E) :
     orthogonalProjection K x =
       Submodule.linearProjOfIsCompl K _ Submodule.isCompl_orthogonal_of_completeSpace x :=
   by rw [← orthogonalProjection_eq_linear_proj]
 
-noncomputable def orthogonalProjection' (U : Submodule 𝕜 E) [CompleteSpace U] : E →L[𝕜] E :=
+noncomputable def orthogonalProjection' (U : Submodule 𝕜 E) [HasOrthogonalProjection U] : E →L[𝕜] E :=
   U.subtypeL.comp (orthogonalProjection U)
 
-theorem orthogonalProjection'_apply (U : Submodule 𝕜 E) [CompleteSpace U] (x : E) :
+theorem orthogonalProjection'_apply (U : Submodule 𝕜 E) [HasOrthogonalProjection U] (x : E) :
     orthogonalProjection' U x = orthogonalProjection U x :=
   rfl
 
@@ -66,24 +66,25 @@ local notation "P" => orthogonalProjection
 local notation "↥P" => orthogonalProjection'
 
 @[simp]
-theorem ContinuousLinearMap.range_toLinearMap {p : E →L[𝕜] E} : LinearMap.range (p.toLinearMap) = LinearMap.range p :=
+theorem ContinuousLinearMap.range_toLinearMap {F : Type*} [NormedAddCommGroup F]
+  [InnerProductSpace 𝕜 F] {p : E →L[𝕜] F} : LinearMap.range (p.toLinearMap) = LinearMap.range p :=
   rfl
 
 open ContinuousLinearMap
 
 @[simp]
-theorem orthogonalProjection.range (U : Submodule 𝕜 E) [CompleteSpace U] :
+theorem orthogonalProjection.range (U : Submodule 𝕜 E) [HasOrthogonalProjection U] :
     LinearMap.range (↥P U) = U := by
   simp_rw [orthogonalProjection', ← range_toLinearMap, coe_comp,
     orthogonalProjection_eq_linear_proj', Submodule.coe_subtypeL, LinearMap.range_comp,
     Submodule.linearProjOfIsCompl_range, Submodule.map_subtype_top]
 
 @[simp]
-theorem orthogonalProjection'_eq (U : Submodule 𝕜 E) [CompleteSpace U] :
+theorem orthogonalProjection'_eq (U : Submodule 𝕜 E) [HasOrthogonalProjection U] :
     ↥P U = U.subtypeL.comp (P U) :=
   rfl
 
-theorem orthogonal_projection'_eq_linear_proj {K : Submodule 𝕜 E} [CompleteSpace K] :
+theorem orthogonal_projection'_eq_linear_proj {K : Submodule 𝕜 E} [HasOrthogonalProjection K] :
     (K.subtypeL.comp (orthogonalProjection K) : E →ₗ[𝕜] E) =
      (K.subtype).comp
         (Submodule.linearProjOfIsCompl K _ Submodule.isCompl_orthogonal_of_completeSpace) :=
@@ -92,7 +93,7 @@ theorem orthogonal_projection'_eq_linear_proj {K : Submodule 𝕜 E} [CompleteSp
   simp_rw [ContinuousLinearMap.coe_coe, LinearMap.comp_apply, ContinuousLinearMap.comp_apply,
     Submodule.subtypeL_apply, Submodule.subtype_apply, orthogonalProjection_eq_linear_proj'']
 
-theorem orthogonalProjection'_eq_linear_proj' {K : Submodule 𝕜 E} [CompleteSpace K] (x : E) :
+theorem orthogonalProjection'_eq_linear_proj' {K : Submodule 𝕜 E} [HasOrthogonalProjection K] (x : E) :
     (orthogonalProjection' K : E →ₗ[𝕜] E) x =
       (K.subtype).comp
         (Submodule.linearProjOfIsCompl K _ Submodule.isCompl_orthogonal_of_completeSpace) x :=

Monlib/LinearAlgebra/IsReal.lean

@@ -5,7 +5,13 @@ Authors: Monica Omar
 -/
 import Mathlib.Algebra.Star.StarAlgHom
 import Mathlib.Algebra.Star.BigOperators
-import Monlib.LinearAlgebra.InnerAut
+-- import Monlib.LinearAlgebra.InnerAut
+import Mathlib.Algebra.Algebra.Spectrum
+import Monlib.LinearAlgebra.End
+import Monlib.Preq.StarAlgEquiv
+import Mathlib.Analysis.RCLike.Basic
+import Mathlib.Analysis.InnerProductSpace.Basic
+import Mathlib.Algebra.Algebra.Bilinear
 import Mathlib.Algebra.Algebra.Basic
 
 #align_import linear_algebra.is_real
@@ -27,11 +33,11 @@ variable {E F K : Type _} [AddCommMonoid E] [StarAddMonoid E] [AddCommMonoid F]
   [Semiring K] [Module K E] [Module K F] [InvolutiveStar K] [StarModule K E] [StarModule K F]
 
 @[simps]
-def LinearMap.real (φ : E →ₗ[K] F) : E →ₗ[K] F
-    where
+def LinearMap.real (φ : E →ₗ[K] F) :
+    E →ₗ[K] F where
   toFun x := star (φ (star x))
-  map_add' x y := by simp only [star_add, map_add]
-  map_smul' r x := by simp only [star_smul, _root_.map_smul, star_star, RingHom.id_apply]
+  map_add' _ _ := by simp only [star_add, map_add]
+  map_smul' _ _ := by simp only [star_smul, _root_.map_smul, star_star, RingHom.id_apply]
 
 theorem LinearMap.isReal_iff (φ : E →ₗ[K] F) : φ.IsReal ↔ φ.real = φ := by
   simp_rw [LinearMap.IsReal, LinearMap.ext_iff, LinearMap.real_apply,

Monlib/LinearAlgebra/MyIps/MatIps.lean

@@ -401,7 +401,7 @@ protected theorem basis_apply (hφ : φ.IsFaithfulPosMap) (ij : n × n) :
     hφ.basis ij = stdBasisMatrix ij.1 ij.2 (1 : ℂ) * hφ.matrixIsPosDef.rpow (-(1 / 2 : ℝ)) := by
   rw [IsFaithfulPosMap.basis, Basis.mk_apply]
 
-local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ x y
+local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ _ _ _ x y
 
 protected noncomputable def toMatrix (hφ : φ.IsFaithfulPosMap) :
     (Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) ≃ₐ[ℂ] Matrix (n × n) (n × n) ℂ :=
@@ -501,14 +501,14 @@ protected theorem toMatrix_symm_apply (hφ : φ.IsFaithfulPosMap)
 
 end Module.Dual.IsFaithfulPosMap
 
-local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ x y
+local notation "|" x "⟩⟨" y "|" => @rankOne ℂ _ _ _ _ _ _ _ x y
 
 /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j k l) -/
 theorem Module.Dual.eq_rankOne_of_faithful_pos_map (hφ : φ.IsFaithfulPosMap)
     (x : Matrix n n ℂ →ₗ[ℂ] Matrix n n ℂ) :
     x =
       ∑ i : n, ∑ j : n, ∑ k : n, ∑ l : n,
-         hφ.toMatrix x (i, j) (k, l) • | hφ.basis (i, j)⟩⟨ hφ.basis (k, l)| :=
+         hφ.toMatrix x (i, j) (k, l) • |hφ.basis (i, j)⟩⟨ hφ.basis (k, l)| :=
   by rw [← Module.Dual.IsFaithfulPosMap.toMatrix_symm_apply, AlgEquiv.symm_apply_apply]
 
 end SingleBlock