zero_rootSpace_eq_top_of_nilpotent

English

For a nilpotent Lie algebra L, the zero root space for the whole algebra equals the whole algebra.

Русский

Для нильпотентной Ли-алгебры L нулевая корневая подпространство равно всему L.

LaTeX

$$$\mathrm{rootSpace}(\top : \mathrm LieSubalgebra R L) 0 = \top$$$

Lean4

theorem zero_rootSpace_eq_top_of_nilpotent [LieRing.IsNilpotent L] : rootSpace (⊤ : LieSubalgebra R L) 0 = ⊤ :=
  zero_genWeightSpace_eq_top_of_nilpotent L

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