Commit 2025-09-24 13:52 5f779bef

View on Github →

feat(LinearAlgebra/Matrix): charpoly splits into IsHermitian.eigenvalues (#29476)

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/HermitianFunctionalCalculus.lean

added theorem Matrix.IsHermitian.charpoly_cfc_eq

Modified Mathlib/LinearAlgebra/Matrix/Spectrum.lean

added theorem Matrix.IsHermitian.charpoly_eq

added theorem Matrix.IsHermitian.eigenvalues_eq_eigenvalues_iff

added theorem Matrix.IsHermitian.eigenvalues₀_antitone

added theorem Matrix.IsHermitian.roots_charpoly_eq_eigenvalues

added theorem Matrix.IsHermitian.roots_charpoly_eq_eigenvalues₀

added theorem Matrix.IsHermitian.sort_roots_charpoly_eq_eigenvalues₀

added theorem Matrix.IsHermitian.splits_charpoly