Theorem LieModule.exists_nontrivial_weightSpace_of_isSolvable

Modification history

2025-01-04 18:40
Mathlib/Algebra/Lie/LieTheorem.lean
feat(Algebra/Lie): add Lie's theorem (#13480) …
Added LieModule.exists_nontrivial_weightSpace_of_isSolvableView on Github →