instSemisimple — Mathlib

English

There is a canonical instance asserting that a Killing Lie algebra with finiteness conditions is semisimple.

Русский

Существует стандартный инстанс, что Ли-алгебра Killing при удовлетворяющих условиям конечности является полупростой.

LaTeX

$$$$ \text{IsSemisimple } K L. $$$$

Lean4

instance instSemisimple [IsKilling K L] [Module.Finite K L] : IsSemisimple K L :=
  by
  apply InvariantForm.isSemisimple_of_nondegenerate (Φ := killingForm K L)
  · exact IsKilling.killingForm_nondegenerate _ _
  · exact LieModule.traceForm_lieInvariant _ _ _
  · exact (LieModule.traceForm_isSymm K L L).isRefl
  · intro I h₁ h₂
    exact h₁.1 <| IsKilling.ideal_eq_bot_of_isLieAbelian I

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