Theorems · Inductive type · nonassociative algebras

LieAlgebra.HasCentralRadical

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

A Lie algebra has central radical if its radical coincides with its center. Such Lie algebras are called reductive, if the coefficients are a field of characteristic zero. Note that there is absolutely [no agreement](https://mathoverflow.net/questions/284713/) on what the label 'reductive' should mean when the coefficients are not a field of characteristic zero.

Defined in

Mathlib.Algebra.Lie.Semisimple.Defs

Cited by

5 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CommRingLieRingLieAlgebra