Theorem LinearMap.isNilpotent_iff_charpoly

Modification history

2024-10-31 09:53
Mathlib/LinearAlgebra/Eigenspace/Zero.lean
feat(LinearAlgebra): nilpotent <-> charpoly = X ^ n (#18417)
Added LinearMap.isNilpotent_iff_charpolyView on Github →