instHasTrivialRadical — Mathlib

English

A simple Lie algebra has a trivial radical (zero radical).

Русский

У простой Ли-алгебры тривиальный радикал.

LaTeX

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

Lean4

instance : HasTrivialRadical R L := by
  rw [hasTrivialRadical_iff_no_abelian_ideals]
  intro I hI
  apply (IsSimple.eq_bot_or_eq_top I).resolve_right
  rintro rfl
  rw [lie_abelian_iff_equiv_lie_abelian LieIdeal.topEquiv] at hI
  exact IsSimple.non_abelian R (L := L) hI

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