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.