coe_killingCompl_top — Mathlib

English

If I is Abelian as a Lie algebra, then I is contained in the Killing complement of the top, i.e., I ≤ killingCompl R L ⊤.

Русский

Если I является абелевой как алгебра Ли, то I вложен в верхний киллинг-комплемент: I ≤ killingCompl R L ⊤.

LaTeX

$$I ≤ LieIdeal.killingCompl R L ⊤$$

Lean4

theorem coe_killingCompl_top : killingCompl R L ⊤ = LinearMap.ker (killingForm R L) :=
  by
  ext x
  simp [LinearMap.ext_iff, LinearMap.BilinForm.IsOrtho, LieModule.traceForm_comm R L L x]

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