lowerCentralSeries — Mathlib

English

The lower central series of Lie submodules of a Lie module is defined by lowerCentralSeries using the top submodule.

Русский

Нижняя централная серия подмодулов Ли m определяется через верхний подмодуль и операцию lcs.

LaTeX

$$lowerCentralSeries(R,L,M) = (⊤ : LieSubmodule R L M).lcs k$$

Lean4

/-- The lower central series of Lie submodules of a Lie module. -/
def lowerCentralSeries : LieSubmodule R L M :=
  (⊤ : LieSubmodule R L M).lcs k

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