Theorems · Theorem · linear algebra

Matrix.IsHermitian.spectrum_real_eq_range_eigenvalues

∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A : Matrix n n 𝕜} [inst_2 : DecidableEq n]
  (hA : A.IsHermitian), spectrum ℝ A = Set.range hA.eigenvalues

The ℝ-spectrum of a Hermitian matrix over RCLike field is the range of the eigenvalue function.

Defined in

Mathlib.Analysis.Matrix.Spectrum

Cited by

1 results in Mathlib

Foundations

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

Assumes

RCLikeFintypeDecidableEq