lowerCentralSeries_succ — Mathlib

English

Let L act on M via a Lie algebra structure over a commutative ring R. The (k+1)-st term of the lower central series of M under L equals the bracket of the entire Lie algebra with the k-th term: γ_{k+1} = [L, γ_k], with γ_0 = M.

Русский

Пусть L действует на M через структуру над R; тогда (k+1)-я члены ниже центральной последовательности равны скобке по всему L с k-й частью: γ_{k+1} = [L, γ_k], где γ_0 = M.

LaTeX

$$$\\\\gamma_{k+1} = [L, \\\\\\gamma_k], \quad \\gamma_0 = M,$$$

Lean4

@[simp]
theorem lowerCentralSeries_succ : lowerCentralSeries R L M (k + 1) = ⁅(⊤ : LieIdeal R L), lowerCentralSeries R L M k⁆ :=
  (⊤ : LieSubmodule R L M).lcs_succ k

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