ker_traceForm_eq_bot_of_isCartanSubalgebra

English

The trace form on Cartan subalgebra is nondegenerate.

Русский

Trace-форма на Cartan-subalgebra невырожденна.

LaTeX

$$$ \\ker\\big(\\text{LieModule.traceForm}\\;R\\;H\\;L\\big) = \\{0\\} \\quad\\text{(on Cartan subalgebra)}$$$

Lean4

@[simp]
theorem ker_traceForm_eq_bot_of_isCartanSubalgebra [IsNoetherian R L] [IsArtinian R L] (H : LieSubalgebra R L)
    [H.IsCartanSubalgebra] : LinearMap.ker (LieModule.traceForm R H L) = ⊥ :=
  ker_restrict_eq_bot_of_isCartanSubalgebra R L H

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