Mathlib Changelog
v4
Changelog
About
Github
Theorem
LieModule.exists_nontrivial_weightSpace_of_isNilpotent
Modification history
2025-01-04 18:40
Mathlib/Algebra/Lie/Weights/Linear.lean
feat(Algebra/Lie): add Lie's theorem (#13480) …
Added
LieModule.exists_nontrivial_weightSpace_of_isNilpotent
View on Github →