subsingleton_of_hasTrivialRadical_lie_abelian

English

If HasTrivialRadical and L is abelian, then L is a subsingleton.

Русский

При наличии тривиального радикала и абелевой Ли-алгебры, она является подмножеством-одним элементом.

LaTeX

$$$(HasTrivialRadical\; R\; L) \Rightarrow (IsLieAbelian\; L \Rightarrow Subsingleton\; L)$$$

Lean4

/-- An abelian Lie algebra with trivial radical is trivial. -/
theorem subsingleton_of_hasTrivialRadical_lie_abelian [HasTrivialRadical R L] [h : IsLieAbelian L] : Subsingleton L :=
  by
  rw [isLieAbelian_iff_center_eq_top R L, center_eq_bot] at h
  exact (LieSubmodule.subsingleton_iff R L L).mp (subsingleton_of_bot_eq_top h)

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