leibniz_lie — Mathlib

English

The Leibniz rule for the bracket of a LieDerivation with LieBracket holds: [x, [D1, D2]] equals [ [x, D1], D2 ] + [ D1, [x, D2] ].

Русский

Правило Лейбница для скобки между x и [D1,D2]: [x,[D1,D2]] = [[x,D1],D2] + [D1,[x,D2]].

LaTeX

$$⟪x, ⟪D1, D2⟫⟫ = ⟪⟪x, D1⟫, D2⟫ + ⟪D1, ⟪x, D2⟫⟫$$

Lean4

protected theorem leibniz_lie (x : L) (D₁ D₂ : LieDerivation R L L) : ⁅x, ⁅D₁, D₂⁆⁆ = ⁅⁅x, D₁⁆, D₂⁆ + ⁅D₁, ⁅x, D₂⁆⁆ :=
  by
  ext y
  simp [-lie_skew, ← lie_skew (D₁ x) (D₂ y), ← lie_skew (D₂ x) (D₁ y), sub_eq_neg_add]

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