ad_pow_lie — Mathlib

English

For all x,y,z in L and n ∈ N, the endomorphism (ad x)^n acting on [y,z] expands as an antidiagonal sum of brackets with iterates of ad x on y and on z.

Русский

Для любых x,y,z в L и n ∈ ℕ оператор (ad x)^n, действующий на [y,z], раскладывается в антидиагональное суммирование скобок с итерациями ad x на 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 ad_pow_lie (x y z : L) (n : ℕ) :
    ((ad R L x) ^ n) ⁅y, z⁆ = ∑ ij ∈ antidiagonal n, n.choose ij.1 • ⁅((ad R L x) ^ ij.1) y, ((ad R L x) ^ ij.2) z⁆ :=
  toEnd_pow_lie _ x y z n

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