Theorem LinearMap.finite_of_det_ne_one

Modification history

2025-10-09 18:05
Mathlib/LinearAlgebra/Determinant.lean
feat(LinearAlgebra): roots of charpoly are the eigenvalues/spectrum (#29478)
Added LinearMap.finite_of_det_ne_oneView on Github →