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

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

In this article we formalize in Mizar [1], [2] the inverse function theorem for the class of C¹ 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 C¹ functions between Banach spaces. We referred to [9], [10], and [3] in the formalization.

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.

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.

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.

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 p² + 1 = q² + r², 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 2²ⁿ + k (n = 1, 2, . . . ) are composite.