<abstract xmlns="http://www.w3.org/1999/xhtml">

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 <italic>D</italic>, is defined generally as a map from a commutative ring <italic>A</italic> to <italic>A</italic>-Module <italic>M</italic> with specific conditions. However we start with simpler case, namely dom <italic>D</italic> = rng <italic>D</italic>. This allows to define a derivation in other rings such as a polynomial ring.
A derivation is a map <italic>D</italic> : <italic>A → A</italic> satisfying the following conditions:
(i) <italic>D</italic>(<italic>x</italic> + <italic>y</italic>) = <italic>Dx</italic> + <italic>Dy</italic>,
(ii) <italic>D</italic>(<italic>xy</italic>) = <italic>xDy</italic> + <italic>yDx</italic>, ∀<italic>x, y</italic> ∈ <italic>A</italic>.
Typical properties are formalized such as:
<disp-formula>
<alternatives>
<graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2021-0001_eq_001.png"></graphic>
<math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="block"><mrow><mi>D</mi><mrow><mo>(</mo><mrow><munderover><mo>∑</mo><mrow><mi>i</mi><mo>=</mo><mn>1</mn></mrow><mi>n</mi></munderover><mrow><msub><mrow><mi>x</mi></mrow><mi>i</mi></msub></mrow></mrow><mo>)</mo></mrow><mo>=</mo><munderover><mo>∑</mo><mrow><mi>i</mi><mo>=</mo><mn>1</mn></mrow><mi>n</mi></munderover><mrow><mi>D</mi><msub><mrow><mi>x</mi></mrow><mi>i</mi></msub></mrow></mrow></math>
<tex-math>D\left( {\sum\limits_{i = 1}^n {{x_i}} } \right) = \sum\limits_{i = 1}^n {D{x_i}}</tex-math>
</alternatives>
</disp-formula>
and
<disp-formula>
<alternatives>
<graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2021-0001_eq_002.png"></graphic>
<math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="block"><mrow><mi>D</mi><mrow><mo>(</mo><mrow><munderover><mo>∏</mo><mrow><mi>i</mi><mo>=</mo><mn>1</mn></mrow><mi>n</mi></munderover><mrow><msub><mrow><mi>x</mi></mrow><mi>i</mi></msub></mrow></mrow><mo>)</mo></mrow><mo>=</mo><munderover><mo>∑</mo><mrow><mi>i</mi><mo>=</mo><mn>1</mn></mrow><mi>n</mi></munderover><mrow><msub><mrow><mi>x</mi></mrow><mn>1</mn></msub><msub><mrow><mi>x</mi></mrow><mn>2</mn></msub><mo>⋯</mo><mi>D</mi><msub><mrow><mi>x</mi></mrow><mi>i</mi></msub><mo>⋯</mo><msub><mrow><mi>x</mi></mrow><mi>n</mi></msub></mrow><mrow><mo>(</mo><mrow><mo>∀</mo><msub><mrow><mi>x</mi></mrow><mi>i</mi></msub><mo>∈</mo><mi>A</mi></mrow><mo>)</mo></mrow><mo>.</mo></mrow></math>
<tex-math>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).</tex-math>
</alternatives>
</disp-formula>
We also formalized the Leibniz Formula for power of derivation <italic>D</italic> :
<disp-formula>
<alternatives>
<graphic xmlns:xlink="http://www.w3.org/1999/xlink" xlink:href="graphic/j_forma-2021-0001_eq_003.png"></graphic>
<math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="block"><mrow><msup><mrow><mi>D</mi></mrow><mi>n</mi></msup><mrow><mo>(</mo><mrow><mi>x</mi><mi>y</mi></mrow><mo>)</mo></mrow><mo>=</mo><munderover><mo>∑</mo><mrow><mi>i</mi><mo>=</mo><mn>0</mn></mrow><mi>n</mi></munderover><mrow><mrow><mo>(</mo><mrow><msubsup><mrow></mrow><mi>i</mi><mi>n</mi></msubsup></mrow><mo>)</mo></mrow><msup><mrow><mi>D</mi></mrow><mi>i</mi></msup><mi>x</mi><msup><mrow><mi>D</mi></mrow><mrow><mi>n</mi><mo>-</mo><mi>i</mi></mrow></msup><mi>y</mi><mo>.</mo></mrow></mrow></math>
<tex-math>{D^n}\left( {xy} \right) = \sum\limits_{i = 0}^n {\left( {_i^n} \right){D^i}x{D^{n - i}}y.}</tex-math>
</alternatives>
</disp-formula>
Lastly applying the definition to the polynomial ring of <italic>A</italic> 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].
</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
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].

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

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

{"article-title":"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],...

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

Publié en ligne: 26 août 2021

Pages: 1 - 8

Accepté: 30 mars 2021

DOI: https://doi.org/10.2478/forma-2021-0001

Mots clés
derivation, Leibniz Formula, derivation of polynomial ring

© 2021 Yasushige Watase, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

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

Publié en ligne: 26 août 2021

Pages: 1 - 8

Accepté: 30 mars 2021

DOI: https://doi.org/10.2478/forma-2021-0001

Mots clésderivation, Leibniz Formula, derivation of polynomial ring

© 2021 Yasushige Watase, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 4.0 International License.

Mots clés
derivation, Leibniz Formula, derivation of polynomial ring