Theorems · Definition · nonassociative algebras

LieModule.nilpotencyLength

(L : Type v) → (M : Type w) → [inst : LieRing L] → [inst_1 : AddCommGroup M] → [LieRingModule L M] → ℕ

Given a nilpotent Lie module M with lower central series M = C₀ ≥ C₁ ≥ ⋯ ≥ Cₖ = ⊥, this is the natural number k (the number of inclusions). For a non-nilpotent module, we use the junk value 0.

Defined in

Mathlib.Algebra.Lie.Nilpotent

Cited by

7 results in Mathlib

Foundations

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

Assumes

LieRingAddCommGroupLieRingModule