Theorems · Definition · linear algebra

Matrix.IsHermitian.eigenvectorBasis

{𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {n : Type u_2} →
      [inst_1 : Fintype n] →
        {A : Matrix n n 𝕜} → [DecidableEq n] → A.IsHermitian → OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)

A choice of an orthonormal basis of eigenvectors of a Hermitian matrix.

Defined in

Mathlib.Analysis.Matrix.Spectrum

Cited by

12 results in Mathlib

Foundations

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

Assumes

RCLikeFintypeDecidableEq