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

Abstract

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 and D(∏i=1nxi)=∑i=1nx1x2⋯Dxi⋯xn(∀xi∈A).

We also formalized the Leibniz Formula for power of derivation D : Dn(xy)=∑i=0n(in)DixDn-iy.

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].