Theorems · Theorem · nonassociative algebras

LieAlgebra.nilpotent_of_nilpotent_quotient

∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I : LieIdeal R L},
  I ≤ LieAlgebra.center R L → LieRing.IsNilpotent (L ⧸ I) → LieRing.IsNilpotent L

A central extension of nilpotent Lie algebras is nilpotent.

Defined in

Mathlib.Algebra.Lie.Nilpotent

Cited by

1 results in Mathlib

Foundations

Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingLieRingLieAlgebra