English
If we compose two endomorphisms corresponding to x and y in L, the k-th iterate lies in the 2k-th term of the lower central series.
Русский
Складывая две концевые модули для x и y, при k-й итерации получаем член 2k-й нижней центральной серии.
LaTeX
$$$\\bigl((toEnd(R,L,M)\\,x) \\circ (toEnd(R,L,M)\\,y)\\bigr)^{[k]}(m) \\in \\operatorname{lowerCentralSeries}(R,L,M,2k)$$$
Lean4
theorem iterate_toEnd_mem_lowerCentralSeries₂ (x y : L) (m : M) (k : ℕ) :
(toEnd R L M x ∘ₗ toEnd R L M y)^[k] m ∈ lowerCentralSeries R L M (2 * k) := by
induction k with
| zero => simp
| succ k ih =>
have hk : 2 * k.succ = (2 * k + 1) + 1 := rfl
simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ', hk, toEnd_apply_apply,
LinearMap.coe_comp, toEnd_apply_apply]
refine LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ?_
exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top y) ih
