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.

Estimated changes