restrict_killingForm — Mathlib

English

Let H be a Lie subalgebra of L. Then the Killing form of L, when restricted to H, coincides with the trace form of H on L.

Русский

Пусть H — подалгебра Ли внутри L. Тогда Killing-форма на L, ограниченная на H, совпадает с trace-формой H на L.

LaTeX

$$$ (killingForm\\;R\\;L)\\restriction H = \\ LieModule.traceForm\\;R\\;H\\;L $$$

Lean4

theorem restrict_killingForm (H : LieSubalgebra R L) : (killingForm R L).restrict H = LieModule.traceForm R H L :=
  rfl

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