Commit 2024-04-23 18:45 ec75ee19

View on Github →

feat(LinearAlgebra/Eigenspace/Zero): results on endomorphisms with eigenvalue 0 (#12373)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Eigenspace/Zero.lean

added theorem IsNilpotent.charpoly_eq_X_pow_finrank

added theorem LinearMap.charpoly_constantCoeff_eq_zero_iff

added theorem LinearMap.charpoly_eq_X_pow_iff

added theorem LinearMap.charpoly_nilpotent_tfae

added theorem LinearMap.finrank_maximalGeneralizedEigenspace

added theorem LinearMap.hasEigenvalue_zero_tfae

added theorem LinearMap.not_hasEigenvalue_zero_tfae