lie_lie — Mathlib

English

The action of a Lie element on a second Lie bracket satisfies the Leibniz-type relation: [ [x,y], m ] = [ x, [ y, m ] ] − [ y, [ x, m ] ].

Русский

Действие элементa Ли на двойной скобке удовлетворяет тождеству Лейбница: [ [x,y], m ] = [ x, [ y, m ] ] − [ y, [ x, m ] ].

LaTeX

$$$[ [x,y], m] = [ x, [y, m] ] - [ y, [x, m] ]$$$

Lean4

@[simp]
theorem lie_lie : ⁅⁅x, y⁆, m⁆ = ⁅x, ⁅y, m⁆⁆ - ⁅y, ⁅x, m⁆⁆ := by rw [leibniz_lie, add_sub_cancel_right]

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