Theorem Matrix.IsHermitian.charpoly_eq

Modification history

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