Theorems · Inductive type · nonassociative algebras

LieAlgebra.HasTrivialRadical

(R : Type u_1) → (L : Type u_2) → [inst : CommRing R] → [inst_1 : LieRing L] → [LieAlgebra R L] → Prop

A Lie algebra has trivial radical if its radical is trivial. This is equivalent to having no non-trivial solvable ideals, and further equivalent to having no non-trivial abelian ideals. In characteristic zero, it is also equivalent to LieAlgebra.IsSemisimple. Note that the label 'semisimple' is apparently not universally agreed [upon](https://mathoverflow.net/questions/149391/on-radicals-of-a-lie-algebra#comment383669_149391) for general coefficients. For example [Seligman, page 15](seligman1967) uses the label for LieAlgebra.HasTrivialRadical, whereas we reserve it for Lie algebras that are a direct sum of simple Lie algebras.

Defined in

Mathlib.Algebra.Lie.Semisimple.Defs

Cited by

11 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CommRingLieRingLieAlgebra