Theorem Matrix.IsHermitian.charpoly_cfc_eq

Modification history

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