center_le_maxNilpotentIdeal — Mathlib

English

Let R be a commutative ring and L a Lie algebra over R. Then the center of L is contained in the largest nilpotent ideal of L.

Русский

Пусть R — коммутативное кольцо, L — Ли-алгебра над R. Тогда центр L включён в максимальный нильпотентный идеал L.

LaTeX

$$$\operatorname{center}(R,L) \le \operatorname{maxNilpotentIdeal}(R,L)$$$

Lean4

theorem center_le_maxNilpotentIdeal : center R L ≤ maxNilpotentIdeal R L :=
  le_sSup (trivialIsNilpotent L (center R L))

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