PhyslibAlpha.ProbabilisticTheory.Algebra.Derivation

Let $E$ be a real vector space (an additive commutative group and a module over $\mathbb{R}$) equipped with a multiplication operation. A linear map $D: E \to E$ is a **derivation** if it satisfies the Leibniz rule: for all $a, b \in E$, $D(ab) = (Da)b + a(Db)$.

Let $E$ be a real vector space equipped with a multiplication operation. The zero linear map $0: E \to E$ is a derivation.

Let $E$ be a real vector space equipped with a multiplication operation. If $D_1, D_2: E \to E$ are linear maps that satisfy the derivation condition (the Leibniz rule), then their sum $D_1 + D_2$ is also a derivation.

Let $E$ be a real vector space equipped with a multiplication operation. If a linear map $D: E \to E$ is a derivation (i.e., it satisfies the Leibniz rule $D(ab) = (Da)b + a(Db)$ for all $a, b \in E$), then its additive inverse $-D$ is also a derivation.

Let $E$ be a real vector space equipped with a multiplication operation. Suppose $D: E \to E$ is a linear map that is a derivation, satisfying the Leibniz rule $D(ab) = (Da)b + a(Db)$ for all $a, b \in E$. Then for any scalar $c \in \mathbb{R}$, the scalar multiple $c \cdot D$ is also a derivation. (Note: This assumes that scalar multiplication and the product on $E$ satisfy the compatibility conditions $(cx)y = c(xy) = x(cy)$).