iInf_lcs_le_of_isNilpotent_quot — Mathlib

English

If M/N is nilpotent, then the infimum over all k of the k-th lower central series terms of M is contained in N.

Русский

Если M/N нильпотентен, то пересечение (или инфимум) всех k-й нижней центральной серией M содержится в N.

LaTeX

$$$\\text{If } \\operatorname{IsNilpotent}_L\\bigl(M/N\\bigr),\\; \\bigl(\\bigwedge_{k} \\lowerCentralSeries_R L M k\\bigr) \\le N.$$$

Lean4

theorem iInf_lcs_le_of_isNilpotent_quot (h : IsNilpotent L (M ⧸ N)) : ⨅ k, lowerCentralSeries R L M k ≤ N :=
  by
  obtain ⟨k, hk⟩ := (isNilpotent_quotient_iff R L M N).mp h
  exact iInf_le_of_le k hk

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