killingForm_apply_apply

Mathlib.Algebra.Lie.TraceForm

URI: https://scilib.ai/kg/mathlib#killingForm_apply_apply

English

For all x,y in L, the Killing form value equals the trace of ad_x composed with ad_y.

Русский

Для всех x,y в L значение киллинговой формы равно следу от композиции ad_x и ad_y.

LaTeX

$$killingForm R L x y = trace R L (ad R L x ∘ₗ ad R L y)$$

Lean4

theorem killingForm_apply_apply (x y : L) : killingForm R L x y = trace R L (ad R L x ∘ₗ ad R L y) :=
  LieModule.traceForm_apply_apply R L L x y

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru