top_isCartanSubalgebra_of_nilpotent

English

If L is nilpotent as a Lie algebra, then the whole algebra L is a Cartan subalgebra of itself.

Русский

Пусть L — нильпотентная алгебра Ли; тогда сама L является подалгеброй Кардана для L.

LaTeX

$$$$ (\text{Nilpotent}(L)) \Rightarrow \operatorname{IsCartanSubalgebra}(\top_L). $$$$

Lean4

/-- A nilpotent Lie algebra is its own Cartan subalgebra. -/
instance top_isCartanSubalgebra_of_nilpotent [LieRing.IsNilpotent L] :
    LieSubalgebra.IsCartanSubalgebra (⊤ : LieSubalgebra R L)
    where
  nilpotent := inferInstance
  self_normalizing := by rw [← top_toLieSubalgebra, normalizer_eq_top, top_toLieSubalgebra]

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