lcs_le_self

Mathlib.Algebra.Lie.Nilpotent

URI: https://scilib.ai/kg/mathlib#LieSubmodule.lcs_le_self

← MathLib Explorer

English

For every k, the k-th lower central series term of N is contained in N.

Русский

Для каждого k член k-й нижней центральной серии подмодуля N содержится в N.

LaTeX

$$$N_{\\mathrm{lcs}(k)} \\le N$$$

Lean4

theorem lcs_le_self : N.lcs k ≤ N := by
  induction k with
  | zero => simp
  | succ k ih =>
    simp only [lcs_succ]
    exact (LieSubmodule.mono_lie_right ⊤ ih).trans (N.lie_le_right ⊤)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru