Theorem LinearMap.det_eq_zero_iff_ker_ne_bot

Modification history

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