Commit 2025-09-16 12:06 3b21e242

View on Github →

feat: generalize LinearMap.finrank_maxGenEigenspace (#29428)

Estimated changes

Modified Mathlib/Algebra/Lie/Rank.lean

Modified Mathlib/LinearAlgebra/Charpoly/Basic.lean

added theorem LinearMap.charpoly_sub_smul

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

added theorem Module.End.maxGenEigenspace_eq_maxGenEigenspace_zero

Modified Mathlib/LinearAlgebra/Eigenspace/Zero.lean

added theorem LinearMap.finrank_eigenspace_le

added theorem LinearMap.finrank_genEigenspace_le

deleted theorem LinearMap.finrank_maxGenEigenspace

added theorem LinearMap.finrank_maxGenEigenspace_eq

added theorem LinearMap.finrank_maxGenEigenspace_zero_eq

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

added theorem Matrix.charpoly_sub_scalar