Theorems · Definition · nonassociative algebras

LieAlgebra.derivedLengthOfIdeal

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

Given a solvable Lie ideal I with derived series I = D₀ ≥ D₁ ≥ ⋯ ≥ Dₖ = ⊥, this is the natural number k (the number of inclusions). For a non-solvable ideal, the value is 0.

Defined in

Mathlib.Algebra.Lie.Solvable

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingLieRingLieAlgebra