lie_jacobi

Mathlib.Algebra.Lie.Basic

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

English

The Jacobi identity holds in any Lie algebra: [x,[y,z]] + [y,[z,x]] + [z,[x,y]] = 0.

Русский

Идентичность Якоби выполняется в любой Lie-алгебре: [x,[y,z]] + [y,[z,x]] + [z,[x,y]] = 0.

LaTeX

$$$[x,[y,z]] + [y,[z,x]] + [z,[x,y]] = 0$$$

Lean4

theorem lie_jacobi : ⁅x, ⁅y, z⁆⁆ + ⁅y, ⁅z, x⁆⁆ + ⁅z, ⁅x, y⁆⁆ = 0 :=
  by
  rw [← neg_neg ⁅x, y⁆, lie_neg z, lie_skew y x, ← lie_skew, lie_lie]
  abel

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

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

Разделы

Аффилиация

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