English
The commutator (Lie bracket) of two derivations D1 and D2 on a in A is again a derivation, defined by [D1, D2](a) = D1(D2(a)) − D2(D1(a)).
Русский
Коммутатор двух производных D1 и D2 по отношению к a является вновь полученной производной: [D1, D2](a) = D1(D2(a)) − D2(D1(a)).
LaTeX
$$$[D_1,D_2](a) = D_1(D_2(a)) - D_2(D_1(a))\quad( a\in A )$, and hence $[D_1,D_2] \in \mathrm{Der}_R(A,A).$$$
Lean4
/-- The commutator of derivations is again a derivation. -/
instance : Bracket (Derivation R A A) (Derivation R A A) :=
⟨fun D1 D2 =>
mk' ⁅(D1 : Module.End R A), (D2 : Module.End R A)⁆ fun a b =>
by
simp only [Ring.lie_def, map_add, Algebra.id.smul_eq_mul, Module.End.mul_apply, leibniz, coeFn_coe,
LinearMap.sub_apply]
ring⟩
