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

#### Search

Open Access

#### On the Intersection of Fields F with F [X ]

Page range: 223 - 228

#### Abstract

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

In the first part we show that an irreducible polynomial

Because

Surprisingly, as we show in this third part, this condition is not automatically true for arbitrary fields _{2} we construct for every field _{n}_{n}_{n}

In the fourth part we finally define field extensions:

#### Keywords

- roots of polynomials
- field extensions
- Kronecker’s construction

#### MSC 2010

- 12E05
- 12F05
- 68T99
- 03B35

Open Access

#### Field Extensions and Kronecker’s Construction

Page range: 229 - 235

#### Abstract

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

In the first part we show that an irreducible polynomial

Because

Surprisingly, as we show in the third part, this condition is not automatically true for arbitrary fields _{2} we construct for every field _{n}_{n} ∩_{n}

In this fourth part we finally define field extensions:

#### Keywords

- roots of polynomials
- field extensions
- Kronecker’s construction

#### MSC 2010

- 12E05
- 12F05
- 68T99
- 03B35

#### Abstract

In this article the notion of the underlying simple graph of a graph (as defined in [8]) is formalized in the Mizar system [5], along with some convenient variants. The property of a graph to be without decorators (as introduced in [7]) is formalized as well to serve as the base of graph enumerations in the future.

#### Keywords

- graph operations
- underlying simple graph

#### MSC 2010

- 68T99
- 03B35
- 05C76

#### Abstract

In this articles adjacency-preserving mappings from a graph to another are formalized in the Mizar system [7], [2]. The generality of the approach seems to be largely unpreceeded in the literature to the best of the author’s knowledge. However, the most important property defined in the article is that of two graphs being isomorphic, which has been extensively studied. Another graph decorator is introduced as well.

#### Keywords

- graph homomorphism
- graph isomorphism

#### MSC 2010

- 05C60
- 68T99
- 03B35

#### Abstract

In [6] partial graph mappings were formalized in the Mizar system [3]. Such mappings map some vertices and edges of a graph to another while preserving adjacency. While this general approach is appropriate for the general form of (multidi)graphs as introduced in [7], a more specialized version for graphs without parallel edges seems convenient. As such, partial vertex mappings preserving adjacency between the mapped verticed are formalized here.

#### Keywords

- graph homomorphism
- graph isomorphism

#### MSC 2010

- 05C60
- 68T99
- 03B35

Open Access

#### Operations of Points on Elliptic Curve in Affine Coordinates

Page range: 315 - 320

#### Abstract

In this article, we formalize in Mizar [1], [2] a binary operation of points on an elliptic curve over

#### Keywords

- elliptic curve
- commutative operation

#### MSC 2010

- 14H52
- 14K05
- 68T99
- 03B35