Theorems · Inductive type · nonassociative algebras

LieAlgebra.IsSimple

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

A Lie algebra is simple if it is irreducible as a Lie module over itself via the adjoint action, and it is non-Abelian.

Defined in

Mathlib.Algebra.Lie.Semisimple.Defs

Cited by

10 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CommRingLieRingLieAlgebra