instIsNilpotentSubtypeMemLieSubmoduleGenWeightSpaceOfNatForallOfIsNoetherian

English

By Engel’s theorem, the zero weight space of a Noetherian Lie module is nilpotent.

Русский

По теореме Энгеля нулевое весовое пространство носят нильпотентный характер.

LaTeX

$$IsNilpotent (genWeightSpace M (0 : L → R))$$

Lean4

/-- By Engel's theorem, the zero weight space of a Noetherian Lie module is nilpotent. -/
instance [IsNoetherian R M] : IsNilpotent L (genWeightSpace M (0 : L → R)) :=
  isNilpotent_iff_forall'.mpr <| isNilpotent_toEnd_genWeightSpace_zero M

Похожие утверждения