ucs_eq_top_iff — Mathlib

English

For any N and k, N.ucs(k) equals the top submodule iff the k-th term of the lower central series of the ambient module is contained in N.

Русский

Для любых N и k подмодуль N.ucs(k) равен верхнему подмодулю тогда и только тогда, когда k-я ступень нижней центральной серии модуля содержится в N.

LaTeX

$$$N.\\mathrm{ucs}(k) = \\top \\iff \\ \mathrm{LieModule.lowerCentralSeries}(R,L,M,k) \\le N$$$

Lean4

theorem ucs_eq_top_iff (k : ℕ) : N.ucs k = ⊤ ↔ LieModule.lowerCentralSeries R L M k ≤ N := by
  rw [eq_top_iff, ← lcs_le_iff]; rfl

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