iterate_toEnd_mem_lowerCentralSeries

English

For x in L, and m in M, the k-th iterate of the endomorphism toEnd(x) applied to m lies in the k-th term of the lower central series.

Русский

Для x в L и m в M, применение k-й итерации концевого отображения toEnd(x) к m только что лежит в k-й нижней центральной серии.

LaTeX

$$$(toEnd(R,L,M)\\,x)^{[k]}(m) \\in \\operatorname{lowerCentralSeries}(R,L,M,k)$$$

Lean4

theorem iterate_toEnd_mem_lowerCentralSeries (x : L) (m : M) (k : ℕ) :
    (toEnd R L M x)^[k] m ∈ lowerCentralSeries R L M k := by
  induction k with
  | zero => simp only [Function.iterate_zero, lowerCentralSeries_zero, LieSubmodule.mem_top]
  | succ k
    ih =>
    simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ', toEnd_apply_apply]
    exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ih

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