toEnd_lie — Mathlib

English

For all x,y,z in a Lie algebra L, the identity (ad x)^n [y,z] equals the antidiagonal expansion: sum over i+j=n of binomial(n,i) [ (ad x)^i y, (ad x)^j z ].

Русский

Для любых x,y,z ∈ L выполняется формула для степени n оператора ad по скобке [y,z] через разложение по антидиагонали.

LaTeX

$$$((\mathrm{ad}_R L x)^n) [y,z] = \sum_{(i,j) \in \mathrm{antidiagonal}(n)} {n \choose i} \,[ (\mathrm{ad}_R L x)^i y, (\mathrm{ad}_R L x)^j z \! ]$$$

Lean4

theorem toEnd_lie (x y : L) (z : M) : (φ x) ⁅y, z⁆ = ⁅ad R L x y, z⁆ + ⁅y, φ x z⁆ := by simp

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