Theorem Matrix.IsHermitian.eigenvalues₀_antitone

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₀_antitoneView on Github →