maxNilpotentIdeal_le_radical — Mathlib

English

Let R be a commutative ring and L a Lie algebra over R. The maximal nilpotent ideal is contained in the solvable radical of L.

Русский

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

LaTeX

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

Lean4

theorem maxNilpotentIdeal_le_radical : maxNilpotentIdeal R L ≤ radical R L :=
  sSup_le_sSup fun I (_ : IsNilpotent L I) ↦ isSolvable_of_isNilpotent I

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