orthogonal_isCompl — Mathlib

English

A finite-dimensional Lie algebra L over a field K is semisimple if it has no nontrivial abelian ideals and there exists a nondegenerate reflexive invariant bilinear form Φ on L.

Русский

Конечномерная Ли-алгебра L над полем K является полупростой, если не имеет ненулевых абелевых идеалов и существует невырожденная рефлексивная инвариантная билинейная форма Φ на L.

LaTeX

$$$$ \text{IsSemisimple}(K,L). $$$$

Lean4

theorem orthogonal_isCompl (I : LieIdeal K L) (hI : IsAtom I) : IsCompl I (orthogonal Φ hΦ_inv I) :=
  by
  rw [← LieSubmodule.isCompl_toSubmodule]
  exact orthogonal_isCompl_toSubmodule Φ hΦ_nondeg hΦ_inv hΦ_refl hL I hI

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