English
The k-th term of the lower central series of the range of toEnd, when viewed as a submodule of M, coincides with the k-th term of the lower central series of L acting on M.
Русский
k-я члена нижней центральной серии диапазона toEnd, рассматриваемого как подмодуль M, совпадает с k-й члена нижней центральной серии L-правящего на M.
LaTeX
$$$\\bigl(\\lowerCentralSeries R (\\operatorname{Subtype} (\\lambda x, x \\in \\operatorname{toEnd}(R,L,M).\\mathrm{range} x) M\\, k\\bigr).toSubmodule = \\lowerCentralSeries R L M k .toSubmodule.$$$
Lean4
/-- The upper (aka ascending) central series.
See also `LieSubmodule.lcs`. -/
def ucs (k : ℕ) : LieSubmodule R L M → LieSubmodule R L M :=
normalizer^[k]
