Theorem Matrix.IsHermitian.eigenvalues_mem_spectrum_real

Modification history

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.eigenvalues_mem_spectrum_realView on Github →