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

Summary 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 = 1 n x i ) = ∑ i = 1 n D x i D\left( {\sum\limits_{i = 1}^n {{x_i}} } \right) = \sum\limits_{i = 1}^n {D{x_i}} and D ( ∏ i = 1 n x i ) = ∑ i = 1 n x 1 x 2 ⋯ D x i ⋯ x n ( ∀ x i ∈ 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 : D n ( x y ) = ∑ i = 0 n ( i n ) D i x D n - i y . {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].