Theorems · Definition · operator theory

LinearMap.IsSymmetric.eigenvalues

{𝕜 : 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 → Fin n → ℝ

The eigenvalues for a self-adjoint operator T on a finite-dimensional inner product space E, sorted in decreasing order

Defined in

Mathlib.Analysis.InnerProductSpace.Spectrum

Cited by

31 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceFiniteDimensional