trivialIsNilpotent

Mathlib.Algebra.Lie.Nilpotent

URI: https://scilib.ai/kg/mathlib#LieModule.trivialIsNilpotent

English

If the Lie action is trivial, then L is nilpotent on M with γ_1 = ⊥.

Русский

Пусть действие Ли тривиально; тогда γ_1 = ⊥ и система нильпотентна.

LaTeX

$$[IsTrivial L M] ⇒ lowerCentralSeries(R,L,M,1) = ⊥$$

Lean4

instance (priority := 100) trivialIsNilpotent [IsTrivial L M] : IsNilpotent L M :=
  ⟨by use 1; simp⟩

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

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

Разделы

Аффилиация

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