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 : LinearMap.IsSymmetric T)
(hp : 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 : LinearMap.IsSymmetric T)
:
T.IsFinitelySemisimple
Symmetric operators are semisimple on finite-dimensional subspaces.