Semisimple operators on inner product spaces

This file is a place to gather results related to semisimplicity of linear operators on inner product spaces.

theorem LinearMap.IsSymmetric.orthogonalComplement_mem_invtSubmodule {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : Module.End 𝕜 E} {p : Submodule 𝕜 E} (hT : IsSymmetric T) (hp : p ∈ T.invtSubmodule) : pᗮ ∈ T.invtSubmodule

The orthogonal complement of an invariant submodule is invariant.

theorem LinearMap.IsSymmetric.isFinitelySemisimple {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : Module.End 𝕜 E} (hT : IsSymmetric T) : T.IsFinitelySemisimple

Symmetric operators are semisimple on finite-dimensional subspaces.