leibniz_lie — Mathlib

English

For x in L1, y in L2, m in M, the iterated bracket satisfies the Leibniz rule: [x, [y,m]] = [[x,y], m] + [y, [x,m]].

Русский

Для x ∈ L1, y ∈ L2, m ∈ M выполняется закон Лейбница: ⁅x, ⁅y, m⁆⁆ = ⁅⁅x,y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆.

LaTeX

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

Lean4

theorem leibniz_lie [Add M] [IsLieTower L₁ L₂ M] (x : L₁) (y : L₂) (m : M) : ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ :=
  IsLieTower.leibniz_lie x y m

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