English
LieDerivation R L M is endowed with a LieRingModule structure with bracket defined by inner R L M (D x) for x ∈ L and D ∈ LieDerivation R L M.
Русский
Ли-производная LieDerivation R L M обладает структурой LieRingModule, скобка задана как inner R L M (D x) для x ∈ L и D ∈ LieDerivation R L M.
LaTeX
$$$\text{LieDerivation.instLieRingModule } R L M$$$
Lean4
/-- The commutator of two Lie derivations on a Lie algebra is a Lie derivation. -/
instance instBracket : Bracket (LieDerivation R L L) (LieDerivation R L L) where
bracket D1
D2 :=
LieDerivation.mk ⁅(D1 : Module.End R L), (D2 : Module.End R L)⁆
(fun a b =>
by
simp only [Ring.lie_def, apply_lie_eq_add, coeFn_coe, LinearMap.sub_apply, Module.End.mul_apply, map_add,
sub_lie, lie_sub, ← lie_skew b]
abel)
