There are quite a few occasions in mathematics, where some form of the Leibniz rule $(fg)'=f'g+fg'$ appears - often in connection with some kind of "differential". Some examples are:
- Of coure the standard Leibnitz rule for two functions $f,g:\mathbb{R}\rightarrow\mathbb{R}$, which we can easily generalize for higher dimensional or holomorphic functions and finaly to functions between manifolds.
- There is also the boundary-formula for the product of two manifolds with Boundary: $\partial(M\times N)=(\partial M \times N)\cup(M\times\partial N)$. There seems to be some connection to the first example via Stokes theorem, but I think it is already unclear wether this formula implies the formula of the first example or vice versa.
- In the case of an algebraic varietie $X$ over a field $k$ we define the tangent space at a point $x\in X$ is defined as the space $D$ of derivations i.e. the space of linear functions $\nu:\mathcal{O}_{X,x}\rightarrow k$ satisfying $\nu(fg)=\nu(f)g(p)+f(p)\nu(g)$. In the case $k=\mathbb{C}$ there is some intuition for this, but the Leibniz rule also seems to be the crutial part of the definition for any field and also tangent spaces seem to do what we want with this definition.
- Finally there is also the Serre-Spectral sequence $\lbrace E_r^{p,q}\rbrace$ in cohomology. It can be equipped with a product structure $E_r^{p,q}\times E_r^{s,t}\rightarrow E_r^{p+s,q+t}$ satisfying the (graded) Leibniz rule $d(xy)=d(x)y+(-1)^{p+q}xd(y)$. I'm quite new to the usage of spectral sequences, so I really don't know if there is any connection to anything connected to differentiation in analyis.
So the Leibniz rule appears in quite a lot of occasions and moreover it seems to be sometimes the crutial part in a definition (note, that in the first case it follows from some other definition whilest in the third example it is a crutial part of the definition). Now I wonder if there is some deeper principle or theory connecting all those cases, or maybe explaining why this formula is so important?
The examples seem to show that the Leibniz formula somehow captures what it means to be a differentiation. I'd hazard that this is because the Leibniz formula combines a sort of linearity with a focus on first-order terms to the exclusion of higher-order terms.