derivedLength — Mathlib

English

The derived length of a Lie algebra L is defined as the derived length of its top Lie ideal, i.e., the entire algebra itself.

Русский

Длина производной Ли-алгебры L определяется как длина производной всего L, то есть самого L.

LaTeX

$$$\mathrm{derivedLength}(R,L) = \mathrm{derivedLengthOfIdeal}(R,L,\top).$$$

Lean4

/-- The derived length of a Lie algebra is the derived length of its 'top' Lie ideal.

See also `LieAlgebra.derivedLength_eq_derivedLengthOfIdeal`. -/
noncomputable abbrev derivedLength : ℕ :=
  derivedLengthOfIdeal R L ⊤

Похожие утверждения