Theorem Matrix.IsHermitian.spectrum_toEuclideanLin

Modification history

2025-08-14 03:55
Mathlib/LinearAlgebra/Matrix/Spectrum.lean
chore(LinearAlgebra/Matrix/Spectrum): result in wrong namespace (#28360) …
Deleted Matrix.IsHermitian.spectrum_toEuclideanLinView on Github →
2024-06-26 17:55
Mathlib/LinearAlgebra/Matrix/Spectrum.lean
feat : added `eigenvalues_mem_spectrum_real` and supporting RCLike coercion results (#13838) …
Added Matrix.IsHermitian.spectrum_toEuclideanLinView on Github →