Derivation of Commutative Rings and the Leibniz Formula for Power of Derivation

In this article we formalize in Mizar [1], [2] a derivation of commutative rings, its definition and some properties. The details are to be referred to [5], [7]. A derivation of a ring, say D, is defined generally as a map from a commutative ring A to A-Module M with specific conditions. However we start with simpler case, namely dom D = rng D. This allows to define a derivation in other rings such as a polynomial ring.

A derivation is a map D : A → A satisfying the following conditions:

(i) D(x + y) = Dx + Dy,

(ii) D(xy) = xDy + yDx, ∀x, y ∈ A.

Typical properties are formalized such as: D(∑i=1nxi)=∑i=1nDxi D\left( {\sum\limits_{i = 1}^n {{x_i}} } \right) = \sum\limits_{i = 1}^n {D{x_i}} and D(∏i=1nxi)=∑i=1nx1x2⋯Dxi⋯xn(∀xi∈A). D\left( {\prod\limits_{i = 1}^n {{x_i}} } \right) = \sum\limits_{i = 1}^n {{x_1}{x_2} \cdots D{x_i} \cdots {x_n}} \left( {\forall {x_i} \in A} \right).

We also formalized the Leibniz Formula for power of derivation D : Dn(xy)=∑i=0n(in)DixDn-iy. {D^n}\left( {xy} \right) = \sum\limits_{i = 0}^n {\left( {_i^n} \right){D^i}x{D^{n - i}}y.}

Lastly applying the definition to the polynomial ring of A and a derivation of polynomial ring was formalized. We mentioned a justification about compatibility of the derivation in this article to the same object that has treated as differentiations of polynomial functions [3].