# Search Results

## Summary

This is the second part of a four-article series containing a Mizar [2], [1] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field *F* and every polynomial *p* ∈ *F* [*X*]*\F* there exists a field extension *E* of *F* such that *p* has a root over *E*. The formalization follows Kronecker’s classical proof using *F* [*X*]*/<p>* as the desired field extension *E* [5], [3], [4].

In the first part we show that an irreducible polynomial *p* ∈ *F* [*X*]*\F* has a root over *F* [*X*]*/<p>*. Note, however, that this statement cannot be true in a rigid formal sense: We do not have *F* ⊆ [*X*]*/ < p >* as sets, so *F* is not a subfield of *F* [*X*]*/<p>*, and hence formally *p* is not even a polynomial over *F* [*X*]*/ < p >*. Consequently, we translate *p* along the canonical monomorphism *ϕ : F → F* [*X*]*/<p>* and show that the translated polynomial *ϕ* (*p*) has a root over *F* [*X*]*/<p>*.

Because *F* is not a subfield of *F* [*X*]*/<p>* we construct in this second part the field (*E \ ϕF* )∪*F* for a given monomorphism *ϕ : F → E* and show that this field both is isomorphic to *F* and includes *F* as a subfield. In the literature this part of the proof usually consists of saying that “one can identify *F* with its image *ϕF* in *F* [*X*]*/<p>* and therefore consider *F* as a subfield of *F* [*X*]*/<p>*”. Interestingly, to do so we need to assume that *F* ∩ *E* = ∅, in particular Kronecker’s construction can be formalized for fields *F* with *F* ∩ *F* [*X*] = ∅.

Surprisingly, as we show in the third part, this condition is not automatically true for arbitray fields *F* : With the exception of _{2} we construct for every field *F* an isomorphic copy *F′* of *F* with *F′* ∩ *F′* [*X*] *≠* ∅. We also prove that for Mizar’s representations of _{n}, and we have _{n} ∩ _{n}[*X*] = ∅, ∩ [*X*] = ∅ and ∩ [*X*] = ∅, respectively.

In the fourth part we finally define field extensions: *E* is a field extension of *F* iff *F* is a subfield of *E*. Note, that in this case we have *F* ⊆ *E* as sets, and thus a polynomial *p* over *F* is also a polynomial over *E*. We then apply the construction of the second part to *F* [*X*]*/<p>* with the canonical monomorphism *ϕ : F → F* [*X*]*/<p>*. Together with the first part this gives - for fields *F* with *F ∩ F* [*X*] = ∅ - a field extension *E* of *F* in which *p* ∈ *F* [*X*]*\F* has a root.

## Summary

This is the first part of a four-article series containing a Mizar [3], [1], [2] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field *F* and every polynomial *p* ∈ *F* [*X*]*\F* there exists a field extension *E* of *F* such that *p* has a root over *E*. The formalization follows Kronecker’s classical proof using *F* [*X*]*/<p>* as the desired field extension *E* [9], [4], [6].

In this first part we show that an irreducible polynomial *p* ∈ *F* [*X*]*\F* has a root over *F* [*X*]*/<p>*. Note, however, that this statement cannot be true in a rigid formal sense: We do not have *F* ⊆ [*X*]*/ < p >* as sets, so *F* is not a subfield of *F* [*X*]*/<p>*, and hence formally *p* is not even a polynomial over *F* [*X*]*/ < p >*. Consequently, we translate *p* along the canonical monomorphism *ϕ*: *F* → *F* [*X*]*/<p>* and show that the translated polynomial *ϕ*(*p*) has a root over *F* [*X*]*/<p>*.

Because *F* is not a subfield of *F* [*X*]*/<p>* we construct in the second part the field (*E \ ϕF* )∪*F* for a given monomorphism *ϕ : F* → *E* and show that this field both is isomorphic to *F* and includes *F* as a subfield. In the literature this part of the proof usually consists of saying that “one can identify *F* with its image *ϕF* in *F* [*X*]*/<p>* and therefore consider *F* as a subfield of *F* [*X*]*/<p>*”. Interestingly, to do so we need to assume that *F ∩ E* =∅, in particular Kronecker’s construction can be formalized for fields *F* with *F \ F* [*X*] =∅.

Surprisingly, as we show in the third part, this condition is not automatically true for arbitray fields *F* : With the exception of _{2} we construct for every field *F* an isomorphic copy *F*
^{′} of *F* with *F′* ∩ *F′* [*X*] *≠*∅. We also prove that for Mizar’s representations of _{n}, and we have _{n} ∩ _{n}[*X*] = ∅, ∩ [*X*] = ∅and ∩ [*X*] = ∅, respectively.

In the fourth part we finally define field extensions: *E* is a field extension of *F* i *F* is a subfield of *E*. Note, that in this case we have *F ⊆ E* as sets, and thus a polynomial *p* over *F* is also a polynomial over *E*. We then apply the construction of the second part to *F* [*X*]*/<p>* with the canonical monomorphism *ϕ : F* → *F* [*X*]*/<p>*. Together with the first part this gives - for fields *F* with *F* ∩ *F* [*X*] = ∅ - a field extension *E* of *F* in which *p* ∈ *F* [*X*]*\F* has a root.

## Summary

This is the third part of a four-article series containing a Mizar [3], [1], [2] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field *F* and every polynomial *p* ∈ *F* [*X*]*\F* there exists a field extension *E* of *F* such that *p* has a root over *E*. The formalization follows Kronecker’s classical proof using *F* [*X*]*/<p>* as the desired field extension *E* [6], [4], [5].

In the first part we show that an irreducible polynomial *p* ∈ *F* [*X*]*\F* has a root over *F* [*X*]*/<p>*. Note, however, that this statement cannot be true in a rigid formal sense: We do not have *F* ⊆ *F* [*X*]*/ < p >* as sets, so *F* is not a subfield of *F* [*X*]*/<p>*, and hence formally *p* is not even a polynomial over *F* [*X*]*/ < p >*. Consequently, we translate *p* along the canonical monomorphism *ϕ*: *F → F* [*X*]*/<p>* and show that the translated polynomial *ϕ* (*p*) has a root over *F* [*X*]*/<p>*.

Because *F* is not a subfield of *F* [*X*]*/<p>* we construct in the second part the field (*E \ ϕF*)∪*F* for a given monomorphism *ϕ*: *F → E* and show that this field both is isomorphic to *F* and includes *F* as a subfield. In the literature this part of the proof usually consists of saying that “one can identify *F* with its image *ϕF* in *F* [*X*]*/<p>* and therefore consider *F* as a subfield of *F* [*X*]*/<p>*”. Interestingly, to do so we need to assume that *F* ∩ *E* = ∅, in particular Kronecker’s construction can be formalized for fields *F* with *F* ∩ *F* [*X*] = ∅.

Surprisingly, as we show in this third part, this condition is not automatically true for arbitrary fields *F* : With the exception of ℤ_{2} we construct for every field *F* an isomorphic copy *F′* of *F* with *F′* ∩ *F′* [*X*] ≠ ∅. We also prove that for Mizar’s representations of ℤ* _{n}*, ℚ and ℝ we have ℤ

*∩ ℤ*

_{n}*[*

_{n}*X*] = ∅, ℚ ∩ ℚ[

*X*] = ∅ and ℝ ∩ ℝ[

*X*] = ∅, respectively.

In the fourth part we finally define field extensions: *E* is a field extension of *F* iff *F* is a subfield of *E*. Note, that in this case we have *F* ⊆ *E* as sets, and thus a polynomial *p* over *F* is also a polynomial over *E*. We then apply the construction of the second part to *F* [*X*]*/<p>* with the canonical monomorphism *ϕ*: *F → F* [*X*]*/<p>*. Together with the first part this gives – for fields *F* with *F* ∩ *F* [*X*] = ∅ – a field extension *E* of *F* in which *p* ∈ *F* [*X*]*\F* has a root.

## Summary

This is the fourth part of a four-article series containing a Mizar [3], [2], [1] formalization of Kronecker’s construction about roots of polynomials in field extensions, i.e. that for every field *F* and every polynomial *p* ∈ *F* [*X*]*\F* there exists a field extension *E* of *F* such that *p* has a root over *E*. The formalization follows Kronecker’s classical proof using *F* [*X*]*/<p>* as the desired field extension *E* [6], [4], [5].

In the first part we show that an irreducible polynomial *p* ∈ *F* [*X*]*\F* has a root over *F* [*X*]*/<p>*. Note, however, that this statement cannot be true in a rigid formal sense: We do not have *F* ⊆ *F* [*X*]*/ < p >* as sets, so *F* is not a subfield of *F* [*X*]*/<p>*, and hence formally *p* is not even a polynomial over *F* [*X*]*/ < p >*. Consequently, we translate *p* along the canonical monomorphism *ϕ*: *F → F* [*X*]*/<p>* and show that the translated polynomial *ϕ* (*p*) has a root over *F* [*X*]*/<p>*.

Because *F* is not a subfield of *F* [*X*]*/<p>* we construct in the second part the field (*E \ ϕF*)∪*F* for a given monomorphism *ϕ*: *F → E* and show that this field both is isomorphic to *F* and includes *F* as a subfield. In the literature this part of the proof usually consists of saying that “one can identify *F* with its image *ϕF* in *F* [*X*]*/<p>* and therefore consider *F* as a subfield of *F* [*X*]*/<p>*”. Interestingly, to do so we need to assume that *F* ∩ *E* = ∅, in particular Kronecker’s construction can be formalized for fields *F* with *F ∩ F* [*X*] = ∅.

Surprisingly, as we show in the third part, this condition is not automatically true for arbitrary fields *F* : With the exception of ℤ_{2} we construct for every field *F* an isomorphic copy *F′* of *F* with *F′ ∩ F′* [*X*] ≠ ∅. We also prove that for Mizar’s representations of ℤ* _{n}*, ℚ and ℝ we have ℤ

*ℤ*

_{n}∩*[*

_{n}*X*] = ∅, ℚ

*∩*ℚ[

*X*] = ∅ and ℝ

*∩*ℝ[

*X*] = ∅, respectively.

In this fourth part we finally define field extensions: *E* is a field extension of *F* iff *F* is a subfield of *E*. Note, that in this case we have *F* ⊆ *E* as sets, and thus a polynomial *p* over *F* is also a polynomial over *E*. We then apply the construction of the second part to *F* [*X*]*/<p>* with the canonical monomorphism *ϕ*: *F → F* [*X*]*/<p>*. Together with the first part this gives – for fields *F* with *F ∩ F* [*X*] = ∅ – a field extension *E* of *F* in which *p* ∈ *F* [*X*]*\F* has a root.

## Summary

In this article we further extend the algebraic theory of polynomial rings in Mizar [1, 2, 3]. We deal with roots and multiple roots of polynomials and show that both the real numbers and finite domains are not algebraically closed [5, 7]. We also prove the identity theorem for polynomials and that the number of multiple roots is bounded by the polynomial’s degree [4, 6].

## Modular Integer Arithmetic

In this article we show the correctness of integer arithmetic based on Chinese Remainder theorem as described e.g. in [11]: Integers are transformed to finite sequences of modular integers, on which the arithmetic operations are performed. Retransformation of the results to the integers is then accomplished by means of the Chinese Remainder theorem. The method presented is a typical example for computing in homomorphic images.

## Summary

In this article we introduce Proth numbers and prove two theorems on such numbers being prime [3]. We also give revised versions of Pocklington’s theorem and of the Legendre symbol. Finally, we prove Pepin’s theorem and that the fifth Fermat number is not prime.

## Summary

In this article we formalize rational functions as pairs of polynomials and define some basic notions including the degree and evaluation of rational functions [8]. The main goal of the article is to provide properties of rational functions necessary to prove a theorem on the stability of networks

## Summary

We introduce ordered rings and fields following Artin-Schreier’s approach using positive cones. We show that such orderings coincide with total order relations and give examples of ordered (and non ordered) rings and fields. In particular we show that polynomial rings can be ordered in (at least) two different ways [8, 5, 4, 9]. This is the continuation of the development of algebraic hierarchy in Mizar [2, 3].

## Summary

We extend the algebraic theory of ordered fields [7, 6] in Mizar [1, 2, 3]: we show that every preordering can be extended into an ordering, i.e. that formally real and ordered fields coincide.We further prove some characterizations of formally real fields, in particular the one by Artin and Schreier using sums of squares [4]. In the second part of the article we define absolute values and the square root function [5].