killingForm_restrict_range_ad_nondegenerate

English

The restriction of the Killing form to the range of the adjoint action is nondegenerate.

Русский

Ограничение формы Киллинга на диапазон действия adjoint не вырождено.

LaTeX

$$((killingForm R 𝔻).restrict (LieDerivation.ad R L).range.toSubmodule).Nondegenerate.$$

Lean4

/-- The restriction of the Killing form of a finite-dimensional Killing Lie algebra to the range of
the adjoint action is nondegenerate. -/
theorem killingForm_restrict_range_ad_nondegenerate : ((killingForm R 𝔻).restrict 𝕀).Nondegenerate :=
  by
  convert LieAlgebra.IsKilling.killingForm_nondegenerate R 𝕀
  exact killingForm_restrict_range_ad R L

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