rootSpace_zero_eq — Mathlib

English

The zero-weight root space of H coincides with H viewed as a Lie submodule: rootSpace(H,0) = H.toLieSubmodule.

Русский

Нулевая весовая корневая подпространство H совпадает с H, рассмотренной как подмодуль Ли: rootSpace(H,0) = H.toLieSubmodule.

LaTeX

$$$\operatorname{rootSpace} \; H\; 0 = H.toLieSubmodule$$$

Lean4

@[simp]
theorem rootSpace_zero_eq (H : LieSubalgebra R L) [H.IsCartanSubalgebra] [IsNoetherian R L] :
    rootSpace H 0 = H.toLieSubmodule := by
  rw [← LieSubmodule.toSubmodule_inj, ← coe_zeroRootSubalgebra, zeroRootSubalgebra_eq_of_is_cartan R L H,
    LieSubalgebra.coe_toLieSubmodule]

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