killingForm_nondegenerate

Mathlib.Algebra.Lie.Killing

URI: https://scilib.ai/kg/mathlib#LieAlgebra.IsKilling.killingForm_nondegenerate

English

The Killing form on a Killing Lie algebra is nondegenerate.

Русский

Форма Killing на Ли-алгебре, обладающей свойством Killing, ненегационная (невыраженная).

LaTeX

$$$$ \text{Killing form } (R,L) \text{ is nondegenerate}. $$$$

Lean4

theorem killingForm_nondegenerate : (killingForm R L).Nondegenerate := by
  simp [LinearMap.BilinForm.nondegenerate_iff_ker_eq_bot]

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

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

Разделы

Аффилиация

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