lowerCentralSeries_map_eq_lcs — Mathlib

English

For any k, the k-th lower central series term of N is bot if and only if the k-th lcs of N is bot.

Русский

Для каждого k: N.lcs k = ⊥ тогда и только тогда, когда lcs k N = ⊥.

LaTeX

$$$N.lcs(k) = \\bot \\;\\iff\\; lcs_k(N) = \\bot$$$

Lean4

theorem lowerCentralSeries_map_eq_lcs : (lowerCentralSeries R L N k).map N.incl = N.lcs k :=
  by
  rw [lowerCentralSeries_eq_lcs_comap, LieSubmodule.map_comap_incl, inf_eq_right]
  apply lcs_le_self

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