coe_zeroRootSubalgebra — Mathlib

English

For a nilpotent Lie subalgebra H, the zero root subalgebra equals the zero-weight root space, i.e., coe zeroRootSubalgebra R L H equals rootSpace H 0.

Русский

Для нильпотентной подалгебры H нулевая корневая подсистема равна пространству нулевого веса: coe_zeroRootSubalgebra R L H = rootSpace H 0.

LaTeX

$$coe_zeroRootSubalgebra : (zeroRootSubalgebra R L H) = rootSpace H 0$$

Lean4

@[simp]
theorem coe_zeroRootSubalgebra : (zeroRootSubalgebra R L H : Submodule R L) = rootSpace H 0 :=
  rfl

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