killingForm — Mathlib

English

The Killing form on a Lie algebra L over R is the trace form taken in the adjoint representation, i.e., it is the trace of ad_x ∘ ad_y.

Русский

Киллингова форма алгебры Ли L над R — это форма следа, получаемая изAdjoint-представления: Killing(x,y) = Tr(ad_x ∘ ad_y).

LaTeX

$$killingForm R L = traceForm R L L$$

Lean4

/-- A finite, free (as an `R`-module) Lie algebra `L` carries a bilinear form on `L`.

This is a specialisation of `LieModule.traceForm` to the adjoint representation of `L`. -/
noncomputable abbrev killingForm : LinearMap.BilinForm R L :=
  LieModule.traceForm R L L

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