English
The lcs of a LieIdeal I on M coincides with the lowerCentralSeries computed in I, via the inclusion map.
Русский
Нижняя центральная серия абела I на M совпадает с нижней центральной серией, вычисляемой в I через вложение.
LaTeX
$$$\operatorname{toSubmodule}(I.lcs M k) = \operatorname{lowerCentralSeries} R I M k$$$
Lean4
theorem coe_lcs_eq [LieModule R L M] : LieSubmodule.toSubmodule (I.lcs M k) = lowerCentralSeries R I M k := by
induction k with
| zero => simp
| succ k
ih =>
simp_rw [lowerCentralSeries_succ, lcs_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
(I.lcs M k).mem_toSubmodule, ih, LieSubmodule.mem_toSubmodule, LieSubmodule.mem_top, true_and,
(I : LieSubalgebra R L).coe_bracket_of_module]
simp
