Theorem Module.End.hasEigenvalue_iff_isRoot_charpoly

Modification history

2025-10-09 18:05
Mathlib/LinearAlgebra/Eigenspace/Charpoly.lean
feat(LinearAlgebra): roots of charpoly are the eigenvalues/spectrum (#29478)
Added Module.End.hasEigenvalue_iff_isRoot_charpolyView on Github →