nilpotent

Mathlib.Algebra.Lie.Nilpotent

URI: https://scilib.ai/kg/mathlib#LieModule.IsNilpotent.nilpotent

English

If L acts nilpotently on M, then the infinite infimum of the lower central series over k is the bottom submodule.

Русский

Если L действует нильпотентно на M, то iInf(lcs_k) = ⊥.

LaTeX

$$$\\bigwedge_k lcs_k = ⊥$$$

Lean4

theorem nilpotent [IsNilpotent L M] : ∃ k, lowerCentralSeries R L M k = ⊥ :=
  (isNilpotent_iff R L M).mp ‹_›

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

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

Разделы

Аффилиация

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