Theorem Matrix.IsHermitian.spectrum_real_eq_range_eigenvalues

Modification history

2025-08-31 17:16
Mathlib/LinearAlgebra/Matrix/Spectrum.lean
chore(LinearAlgebra/Matrix/HermitianFunctionalCalculus): moving and renaming stuff (#28401) …
Added Matrix.IsHermitian.spectrum_real_eq_range_eigenvaluesView on Github →