Theorems · Definition · operator theory

LinearMap.IsSymmetric.eigenvectorBasis

{𝕜 : Type u_3} →
  [inst : RCLike 𝕜] →
    {E : Type u_4} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {T : E →ₗ[𝕜] E} →
            [FiniteDimensional 𝕜 E] → {n : ℕ} → T.IsSymmetric → Module.finrank 𝕜 E = n → OrthonormalBasis (Fin n) 𝕜 E

A choice of orthonormal basis of eigenvectors for self-adjoint operator T on a finite-dimensional inner product space E. Eigenvectors are sorted in decreasing order of their eigenvalues.

Defined in

Mathlib.Analysis.InnerProductSpace.Spectrum

Cited by

11 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceFiniteDimensional