Theorems · Theorem · linear algebra

Matrix.IsHermitian.spectral_theorem

∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian),
  A =
    ((Unitary.conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary) (Matrix.diagonal (RCLike.ofReal ∘ hA.eigenvalues))

Diagonalization theorem, spectral theorem for matrices; A Hermitian matrix can be diagonalized by a change of basis. For the spectral theorem on linear maps, see LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply.

Defined in

Mathlib.Analysis.Matrix.Spectrum

Cited by

10 results in Mathlib

Foundations

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

Assumes

RCLikeFintypeDecidableEq