ad_lie — Mathlib

English

For all x,y,z in a Lie algebra L, the identity (ad x) [y,z] equals [ (ad x) y, z ] + [ y, (ad x) z ].

Русский

Для всех x,y,z в Ли-алгебре L выполняется тождество (ad x)[y,z] = [ (ad x) y, z ] + [ y, (ad x) z ].

LaTeX

$$$(\mathrm{ad}_R L x) \, [y,z] = [ (\mathrm{ad}_R L x) y, z ] + [ y, (\mathrm{ad}_R L x) z ]$$$

Lean4

theorem ad_lie (x y z : L) : (ad R L x) ⁅y, z⁆ = ⁅ad R L x y, z⁆ + ⁅y, ad R L x z⁆ :=
  toEnd_lie _ x y z

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