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

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 arbitray fields _{2} we construct for every field _{n}, and we have _{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