English
The collection of Lie Derivations is closed under subtraction: for any Lie Derivations D1, D2, the difference D1 − D2 is again a Lie Derivation R L M, defined by (D1 − D2)(a) = D1(a) − D2(a) for all a in L.
Русский
Множество производных Ли замкнуто по вычитанию: для любых D1, D2 производная D1 − D2 снова является производной Ли в пространстве L, заданной для всех a ∈ L как (D1(a) − D2(a)).
LaTeX
$$$\forall D_1,D_2:\; (D_1 - D_2) \; \text{is a Lie Derivation and } (D_1 - D_2)(a) = D_1(a) - D_2(a) \text{ for all } a \in L.$$$
Lean4
instance instSub : Sub (LieDerivation R L M) :=
⟨fun D1 D2 =>
mk (D1 - D2 : L →ₗ[R] M) fun a b => by
simp only [LinearMap.sub_apply, coeFn_coe, apply_lie_eq_sub, lie_sub, sub_sub_sub_comm]⟩
