isNilpotent_iff_forall — Mathlib

English

Let L be a Lie algebra over R which is Noetherian as an R-module. Then L is nilpotent iff for every x in L the adjoint endomorphism ad_x: L → L is nilpotent.

Русский

Пусть L — Lie-алгебра над R, и L является Noetherian как R-модуль. Тогда L нильпотентна тогда и только тогда, когда для каждого x ∈ L отображение ad_x: L → L является нильпотентным.

LaTeX

$$$[IsNoetherian_R_L] \Rightarrow \left( \operatorname{LieRing.IsNilpotent} L \iff \forall x \in L, \operatorname{IsNilpotent}\big(\operatorname{ad}_{R,L}(x)\big) \right)$$$

Lean4

/-- Engel's theorem. -/
theorem isNilpotent_iff_forall [IsNoetherian R L] : LieRing.IsNilpotent L ↔ ∀ x, IsNilpotent <| LieAlgebra.ad R L x :=
  LieModule.isNilpotent_iff_forall

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