of_associative_ring_bracket

Mathlib.Algebra.Lie.OfAssociative

URI: https://scilib.ai/kg/mathlib#LieRing.of_associative_ring_bracket

English

In an associative ring A, the Lie bracket [x,y] defined by [x,y] = xy - yx satisfies the Lie ring axioms.

Русский

В ассоциативном кольце A скобка Ли [x,y] = xy - yx удовлетворяет аксиомам Ли-кольца.

LaTeX

$$$ [x,y] = xy - yx \\quad (x,y \\in A) $$$

Lean4

theorem of_associative_ring_bracket (x y : A) : ⁅x, y⁆ = x * y - y * x :=
  rfl

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

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

Разделы

Аффилиация

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