Theorems · Definition · nonassociative algebras

LieAlgebra.derivedSeriesOfIdeal

(R : Type u) →
  (L : Type v) →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → ℕ → LieIdeal R L → LieIdeal R L

A generalisation of the derived series of a Lie algebra, whose zeroth term is a specified ideal. It can be more convenient to work with this generalisation when considering the derived series of an ideal since it provides a type-theoretic expression of the fact that the terms of the ideal's derived series are also ideals of the enclosing algebra. See also LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_comap and LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_map below.

Defined in

Mathlib.Algebra.Lie.Solvable

Cited by

28 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

CommRingLieRingLieAlgebra