instIsLieAbelianOfIsCartanSubalgebra

English

If the trace form on Cartan subalgebra is nondegenerate, then the Cartan subalgebra is abelian.

Русский

Если trace-форма на Cartan-subalgebra невырожденна, то сама Cartan-subalgebra абелева.

LaTeX

$$$ [H,H] = 0 \quad\\text{in } H$$$

Lean4

instance instIsLieAbelianOfIsCartanSubalgebra [IsDomain R] [IsPrincipalIdealRing R] [IsArtinian R L]
    (H : LieSubalgebra R L) [H.IsCartanSubalgebra] : IsLieAbelian H :=
  LieModule.isLieAbelian_of_ker_traceForm_eq_bot R H L <| ker_restrict_eq_bot_of_isCartanSubalgebra R L H

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