Theorem Matrix.IsHermitian.eigenvalues_eq_eigenvalues_iff

Modification history

2025-09-24 13:52
Mathlib/LinearAlgebra/Matrix/Spectrum.lean
feat(LinearAlgebra/Matrix): `charpoly` splits into `IsHermitian.eigenvalues` (#29476)
Added Matrix.IsHermitian.eigenvalues_eq_eigenvalues_iffView on Github →