instIsSemisimple — Mathlib

English

A simple Lie algebra is semisimple.

Русский

Простая Ли-алгебра является полусемисемптической.

LaTeX

$$$(IsSimple R L) \Rightarrow (IsSemisimple R L)$$$

Lean4

/-- A simple Lie algebra is semisimple. -/
instance (priority := 100) instIsSemisimple [IsSimple R L] : IsSemisimple R L :=
  by
  constructor
  · simp
  · simpa using sSupIndep_singleton _
  · intro I hI₁ hI₂
    apply IsSimple.non_abelian (R := R) (L := L)
    rw [IsSimple.isAtom_iff_eq_top] at hI₁
    rwa [hI₁, lie_abelian_iff_equiv_lie_abelian LieIdeal.topEquiv] at hI₂

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