Theorems · Theorem · operator theory

LinearMap.IsSymmetric.directSum_isInternal_of_commute

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {A B : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E],
  A.IsSymmetric →
    B.IsSymmetric →
      Commute A B → DirectSum.IsInternal fun i => Module.End.eigenspace A i.2 ⊓ Module.End.eigenspace B i.1

Given a commuting pair of symmetric linear operators on a finite-dimensional inner product space, the space decomposes as an internal direct sum of simultaneous eigenspaces of these operators.

Defined in

Mathlib.Analysis.InnerProductSpace.JointEigenspace

Cited by

0 results in Mathlib

Foundations

Depth 206 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceFiniteDimensional