Commit 2025-10-09 18:05 afac0c21

View on Github →

feat(LinearAlgebra): roots of charpoly are the eigenvalues/spectrum (#29478)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/Determinant.lean

modified theorem LinearMap.bot_lt_ker_of_det_eq_zero

added theorem LinearMap.det_eq_zero_iff_ker_ne_bot

added theorem LinearMap.finite_of_det_ne_one

Created Mathlib/LinearAlgebra/Eigenspace/Charpoly.lean

added theorem Module.End.hasEigenvalue_iff_isRoot_charpoly

added theorem Module.End.mem_spectrum_iff_isRoot_charpoly

Modified Mathlib/LinearAlgebra/Eigenspace/Matrix.lean

added theorem LinearMap.spectrum_toMatrix'

added theorem LinearMap.spectrum_toMatrix

modified theorem Matrix.maxGenEigenspace_toLin'_diagonal_eq_eigenspace

modified theorem Matrix.maxGenEigenspace_toLin_diagonal_eq_eigenspace

added theorem Matrix.spectrum_toLin'

added theorem Matrix.spectrum_toLin

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean

modified theorem Matrix.det_eq_prod_roots_charpoly

modified theorem Matrix.det_eq_prod_roots_charpoly_of_splits

added theorem Matrix.mem_spectrum_iff_isRoot_charpoly

added theorem Matrix.mem_spectrum_of_isRoot_charpoly

modified theorem Matrix.trace_eq_sum_roots_charpoly

modified theorem Matrix.trace_eq_sum_roots_charpoly_of_splits