Volume 29 (2021): Issue 1 (April 2021)

Journal Details
Format
Journal
eISSN
1898-9934
First Published
09 Jun 2008
Publication timeframe
4 times per year
Languages
English

6 Articles
Open Access

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

Published Online: 26 Aug 2021
Page range: 1 - 8

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, yA.

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=1nx1x2Dxixn(xiA). 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].

Keywords

• derivation
• Leibniz Formula
• derivation of polynomial ring

• 13B25
• 13N15
• 68V20
Open Access

Inverse Function Theorem. Part I1

Published Online: 26 Aug 2021
Page range: 9 - 19

Abstract

In this article we formalize in Mizar [1], [2] the inverse function theorem for the class of C1 functions between Banach spaces. In the first section, we prove several theorems about open sets in real norm space, which are needed in the proof of the inverse function theorem. In the next section, we define a function to exchange the order of a product of two normed spaces, namely 𝔼 ↶ ≂ (x, y) ∈ X × Y ↦ (y, x) ∈ Y × X, and formalized its bijective isometric property and several differentiation properties. This map is necessary to change the order of the arguments of a function when deriving the inverse function theorem from the implicit function theorem proved in [6].

In the third section, using the implicit function theorem, we prove a theorem that is a necessary component of the proof of the inverse function theorem. In the last section, we finally formalized an inverse function theorem for class of C1 functions between Banach spaces. We referred to [9], [10], and [3] in the formalization.

Keywords

• inverse function theorem
• Lipschitz continuity
• differentiability
• implicit function
• inverse function

• 26B10
• 47A05
• 47J07
• 68V20
Open Access

Miscellaneous Graph Preliminaries. Part I

Published Online: 26 Aug 2021
Page range: 21 - 38

Abstract

This article contains many auxiliary theorems which were missing in the Mizar Mathematical Library to the best of the author’s knowledge. Most of them regard graph theory as formalized in the GLIB series and are needed in upcoming articles.

• graph

• 05C99
• 68V20
Open Access

Algebraic Extensions

Published Online: 26 Aug 2021
Page range: 39 - 47

Abstract

In this article we further develop field theory in Mizar [1], [2], [3] towards splitting fields. We deal with algebraic extensions [4], [5]: a field extension E of a field F is algebraic, if every element of E is algebraic over F. We prove amongst others that finite extensions are algebraic and that field extensions generated by a finite set of algebraic elements are finite. From this immediately follows that field extensions generated by roots of a polynomial over F are both finite and algebraic. We also define the field of algebraic elements of E over F and show that this field is an intermediate field of E|F.

Keywords

• algebraic extensions
• finite extensions
• field of algebraic numbers

• 12F05
• 68V20
Open Access

Functional Space Consisted by Continuous Functions on Topological Space

Published Online: 26 Aug 2021
Page range: 49 - 62

Abstract

In this article, using the Mizar system [1], [2], first we give a definition of a functional space which is constructed from all continuous functions defined on a compact topological space [5]. We prove that this functional space is a Banach space [3]. Next, we give a definition of a function space which is constructed from all continuous functions with bounded support. We also prove that this function space is a normed space.

Keywords

• continuous function space
• compact topological space
• Banach space

• 46E10
• 68V20
Open Access

Elementary Number Theory Problems. Part II

Published Online: 26 Aug 2021
Page range: 63 - 68

Abstract

In this paper problems 14, 15, 29, 30, 34, 78, 83, 97, and 116 from [6] are formalized, using the Mizar formalism [1], [2], [3]. Some properties related to the divisibility of prime numbers were proved. It has been shown that the equation of the form p2 + 1 = q2 + r2, where p, q, r are prime numbers, has at least four solutions and it has been proved that at least five primes can be represented as the sum of two fourth powers of integers. We also proved that for at least one positive integer, the sum of the fourth powers of this number and its successor is a composite number. And finally, it has been shown that there are infinitely many odd numbers k greater than zero such that all numbers of the form 22n + k (n = 1, 2, . . . ) are composite.

Keywords

• number theory
• divisibility
• primes

• 11A41
• 03B35
• 68V20