English
The set of left-invariant derivations on a Lie group carries a Lie ring structure, with the bracket defined by the commutator of derivations and the usual bilinearity and Leibniz properties.
Русский
Множество левых инвариантных выводов на Lie-группе образует структуру Ли-кольца, скобка задаётся коммутатором вывода и удовлетворяет обычным свойствам билинейности и произведения Ли.
LaTeX
$$$\mathrm{LeftInvariantDerivation}(I,G)$ is a Lie ring with bracket defined by the commutator of derivations.$$
Lean4
instance : LieRing (LeftInvariantDerivation I G)
where
add_lie X Y
Z := by
ext1
simp only [commutator_apply, coe_add, Pi.add_apply, map_add]
ring
lie_add X Y
Z := by
ext1
simp only [commutator_apply, coe_add, Pi.add_apply, map_add]
ring
lie_self X := by ext1; simp only [commutator_apply, sub_self]; rfl
leibniz_lie X Y
Z := by
ext1
simp only [commutator_apply, coe_add, map_sub, Pi.add_apply]
ring
