instIsKilling_range_ad — Mathlib

English

The range of the adjoint action on a Killing Lie algebra is itself a Killing Lie algebra.

Русский

Диапазон действия сопряженного отображения на Killing-алгебре сам является Killing-алгеброй.

LaTeX

$$IsKilling R 𝕀, where 𝕀 = Range(ad_{R,L}).$$

Lean4

instance instIsKilling_range_ad : LieAlgebra.IsKilling R 𝕀 :=
  (LieEquiv.ofInjective (ad R L) (injective_ad_of_center_eq_bot <| by simp)).isKilling

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