Theorem LieModule.exists_forall_lie_eq_smul_of_weightSpace_ne_bot

Modification history

2024-04-20 13:53
Mathlib/Algebra/Lie/Weights/Linear.lean
feat: define the coroots of a semisimple Lie algebra (#10893) …
Deleted LieModule.exists_forall_lie_eq_smul_of_weightSpace_ne_botView on Github →
2023-11-30 16:55
Mathlib/Algebra/Lie/Weights/Linear.lean
feat: existence of simultaneous eigenvectors given simultaneous generalized eigenvectors for Lie modules (#8745)
Added LieModule.exists_forall_lie_eq_smul_of_weightSpace_ne_botView on Github →