English
Let R be a commutative ring, L a Lie algebra over R, and M a Lie L-module which is Noetherian as an R-module. Then M is nilpotent as a Lie module iff for every x in L the endomorphism of M given by the action of x is nilpotent.
Русский
Пусть R — коммутативное кольцо, L — Lie-алгебра над R, и M — Lie-модуль над L, который является Noetherian как R-модуль. Тогда M нильпотентна как Lie-модуль iff для каждого x ∈ L соответствующий оператор ρ_x: M → M, заданный действием x, является нильпотентным.
LaTeX
$$$[IsNoetherian_R_M] \Rightarrow \left( \operatorname{LieModule.IsNilpotent} L M \iff \forall x \in L, \operatorname{IsNilpotent}\big(\text{toEnd } R L M x\big) \right)$$$
Lean4
/-- Engel's theorem. -/
theorem isNilpotent_iff_forall' [IsNoetherian R M] :
LieModule.IsNilpotent L M ↔ ∀ x, _root_.IsNilpotent <| toEnd R L M x := by
rw [← isNilpotent_range_toEnd_iff (R := R), LieModule.isNilpotent_iff_forall (R := R)]; simp
