Theorem Matrix.IsHermitian.roots_charpoly_eq_eigenvalues₀

Modification history

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