Theorems · Definition · nonassociative algebras

LieAlgebra.derivedAbelianOfIdeal

{R : Type u} →
  {L : Type v} → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LieIdeal R L → LieIdeal R L

Given a solvable Lie ideal I with derived series I = D₀ ≥ D₁ ≥ ⋯ ≥ Dₖ = ⊥, this is the k-1th term in the derived series (and is therefore an Abelian ideal contained in I). For a non-solvable ideal, this is the zero ideal, ⊥.

Defined in

Mathlib.Algebra.Lie.Solvable

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingLieRingLieAlgebra