instIsIrreducible — Mathlib

English

In a simple Lie algebra, the whole algebra (top ideal) is an atom in the lattice of ideals.

Русский

В простой Ли-алгебре весь алгебра является атомом в решетке идеалов.

LaTeX

$$IsAtom (⊤ : LieIdeal R L)$$

Lean4

instance : LieModule.IsIrreducible R L L :=
  by
  suffices Nontrivial (LieIdeal R L) from ⟨IsSimple.eq_bot_or_eq_top⟩
  rw [LieSubmodule.nontrivial_iff, ← not_subsingleton_iff_nontrivial]
  have _i : ¬IsLieAbelian L := IsSimple.non_abelian R
  contrapose! _i
  infer_instance

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