le_zeroRootSubalgebra — Mathlib

English

For a nilpotent subalgebra H of a Lie algebra L over R, every element of H lies in the zeroRootSubalgebra R L H; i.e., H is contained in the subalgebra consisting of elements with zero root relative to H.

Русский

Для нильпотентной подалгебры H внутри Ли-алгебры L над R верно, что каждый элемент H принадлежит нулевому корневому подалгебре, то есть H ⊆ zeroRootSubalgebra R L H.

LaTeX

$$$H \leq zeroRootSubalgebra\, R\, L\, H$$$

Lean4

theorem le_zeroRootSubalgebra : H ≤ zeroRootSubalgebra R L H :=
  by
  rw [← LieSubalgebra.toSubmodule_le_toSubmodule, ← H.coe_toLieSubmodule, coe_zeroRootSubalgebra,
    LieSubmodule.toSubmodule_le_toSubmodule]
  exact toLieSubmodule_le_rootSpace_zero R L H

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