Commit 2025-08-31 17:16 602163a0
View on Github →chore(LinearAlgebra/Matrix/HermitianFunctionalCalculus): moving and renaming stuff (#28401)
This moves the results about spectrum
from Matrix/HermitianFunctionalCalculus
to Matrix/Spectrum
so that we can use them in other files.
This also renames Matrix.IsHermitian.eigenvalues_eq_spectrum_real
, as it should be Matrix.IsHermitian.spectrum_real_eq_range_eigenvalues
since it states: spectrum ℝ A = Set.range hA.eigenvalues
and not the other way around.
Also added a result for what the 𝕜
-spectrum of a Hermitian matrix is.