Theorem Matrix.IsHermitian.spectrum_eq_image_range

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_eq_image_rangeView on Github →