{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T13:38:32Z","timestamp":1777469912973,"version":"3.51.4"},"reference-count":10,"publisher":"Walter de Gruyter GmbH","issue":"2","license":[{"start":{"date-parts":[[2020,7,1]],"date-time":"2020-07-01T00:00:00Z","timestamp":1593561600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020,7,1]]},"abstract":"Summary<\/jats:title>\n \n In [7], [9], [10] we presented a formalization of Kronecker\u2019s construction of a field extension\n E<\/jats:italic>\n for a field\n F<\/jats:italic>\n in which a given polynomial\n p \u2208 F<\/jats:italic>\n [\n X<\/jats:italic>\n ]\n \\F<\/jats:italic>\n has a root [5], [6], [3]. A drawback of our formalization was that it works only for polynomial-disjoint fields, that is for fields\n F<\/jats:italic>\n with\n F<\/jats:italic>\n \u2229\n F<\/jats:italic>\n [\n X<\/jats:italic>\n ] = \u2205. The main purpose of Kronecker\u2019s construction is that by induction one gets a field extension of\n F<\/jats:italic>\n in which\n p<\/jats:italic>\n splits into linear factors. For our formalization this means that the constructed field extension\n E<\/jats:italic>\n again has to be polynomial-disjoint.\n <\/jats:p>\n \n In this article, by means of Mizar system [2], [1], we first analyze whether our formalization can be extended that way. Using the field of polynomials over\n F<\/jats:italic>\n with degree smaller than the degree of\n p<\/jats:italic>\n to construct the field extension\n E<\/jats:italic>\n does not work: In this case\n E<\/jats:italic>\n is polynomial-disjoint if and only if\n p<\/jats:italic>\n is linear. Using\n F<\/jats:italic>\n [\n X<\/jats:italic>\n ]\n \/<p><\/jats:italic>\n one can show that for\n F<\/jats:italic>\n = \u211a and\n F<\/jats:italic>\n = \u2124\n \n n<\/jats:sub>\n <\/jats:italic>\n the constructed field extension\n E<\/jats:italic>\n is again polynomial-disjoint, so that in particular algebraic number fields can be handled.\n <\/jats:p>\n \n For the general case we then introduce renamings of sets\n X<\/jats:italic>\n as injective functions\n f<\/jats:italic>\n with dom(\n f<\/jats:italic>\n ) =\n X<\/jats:italic>\n and rng(\n f<\/jats:italic>\n ) \u2229 (\n X<\/jats:italic>\n \u222a\n Z<\/jats:italic>\n ) = \u2205 for an arbitrary set\n Z<\/jats:italic>\n . This, finally, allows to construct a field extension\n E<\/jats:italic>\n of an arbitrary field\n F<\/jats:italic>\n in which a given polynomial\n p<\/jats:italic>\n \u2208\n F<\/jats:italic>\n [\n X<\/jats:italic>\n ]\n \\F<\/jats:italic>\n splits into linear factors. Note, however, that to prove the existence of renamings we had to rely on the axiom of choice.\n <\/jats:p>","DOI":"10.2478\/forma-2020-0012","type":"journal-article","created":{"date-parts":[[2021,4,6]],"date-time":"2021-04-06T23:35:49Z","timestamp":1617752149000},"page":"129-135","source":"Crossref","is-referenced-by-count":5,"title":["Renamings and a Condition-free Formalization of Kronecker\u2019s Construction"],"prefix":"10.2478","volume":"28","author":[{"given":"Christoph","family":"Schwarzweller","sequence":"first","affiliation":[{"name":"Institute of Informatics , University of Gda\u0144sk , Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2021,1,9]]},"reference":[{"key":"2026042801400956421_j_forma-2020-0012_ref_001_w2aab3b7b1b1b6b1ab1ab1Aa","doi-asserted-by":"crossref","unstructured":"[1] Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, Karol P\u0105k, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261\u2013279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007\/978-3-319-20615-8_17.10.1007\/978-3-319-20615-8_17","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"2026042801400956421_j_forma-2020-0012_ref_002_w2aab3b7b1b1b6b1ab1ab2Aa","doi-asserted-by":"crossref","unstructured":"[2] Grzegorz Bancerek, Czes\u0142aw Byli\u0144ski, Adam Grabowski, Artur Korni\u0142owicz, Roman Matuszewski, Adam Naumowicz, and Karol P\u0105k. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9\u201332, 2018. doi:10.1007\/s10817-017-9440-6.10.1007\/s10817-017-9440-6604425130069070","DOI":"10.1007\/s10817-017-9440-6"},{"key":"2026042801400956421_j_forma-2020-0012_ref_003_w2aab3b7b1b1b6b1ab1ab3Aa","unstructured":"[3] Nathan Jacobson. Basic Algebra I. Dover Books on Mathematics, 1985."},{"key":"2026042801400956421_j_forma-2020-0012_ref_004_w2aab3b7b1b1b6b1ab1ab4Aa","unstructured":"[4] Artur Korni\u0142owicz. Quotient rings. Formalized Mathematics, 13(4):573\u2013576, 2005."},{"key":"2026042801400956421_j_forma-2020-0012_ref_005_w2aab3b7b1b1b6b1ab1ab5Aa","doi-asserted-by":"crossref","unstructured":"[5] Heinz L\u00fcneburg. Gruppen, Ringe, K\u00f6rper: Die grundlegenden Strukturen der Algebra. Oldenbourg Verlag, 1999.10.1524\/9783486599022","DOI":"10.1524\/9783486599022"},{"key":"2026042801400956421_j_forma-2020-0012_ref_006_w2aab3b7b1b1b6b1ab1ab6Aa","unstructured":"[6] Knut Radbruch. Algebra I. Lecture Notes, University of Kaiserslautern, Germany, 1991."},{"key":"2026042801400956421_j_forma-2020-0012_ref_007_w2aab3b7b1b1b6b1ab1ab7Aa","doi-asserted-by":"crossref","unstructured":"[7] Christoph Schwarzweller. On roots of polynomials over F [X]\/ \u3008 p\u3009. Formalized Mathematics, 27(2):93\u2013100, 2019. doi:10.2478\/forma-2019-0010.10.2478\/forma-2019-0010","DOI":"10.2478\/forma-2019-0010"},{"key":"2026042801400956421_j_forma-2020-0012_ref_008_w2aab3b7b1b1b6b1ab1ab8Aa","doi-asserted-by":"crossref","unstructured":"[8] Christoph Schwarzweller. On monomorphisms and subfields. Formalized Mathematics, 27(2):133\u2013137, 2019. doi:10.2478\/forma-2019-0014.10.2478\/forma-2019-0014","DOI":"10.2478\/forma-2019-0014"},{"key":"2026042801400956421_j_forma-2020-0012_ref_009_w2aab3b7b1b1b6b1ab1ab9Aa","doi-asserted-by":"crossref","unstructured":"[9] Christoph Schwarzweller. Field extensions and Kronecker\u2019s construction. Formalized Mathematics, 27(3):229\u2013235, 2019. doi:10.2478\/forma-2019-0022.10.2478\/forma-2019-0022","DOI":"10.2478\/forma-2019-0022"},{"key":"2026042801400956421_j_forma-2020-0012_ref_010_w2aab3b7b1b1b6b1ab1ac10Aa","doi-asserted-by":"crossref","unstructured":"[10] Christoph Schwarzweller. Representation matters: An unexpected property of polynomial rings and its consequences for formalizing abstract field theory. In M. Ganzha, L. Maciaszek, and M. Paprzycki, editors, Proceedings of the 2018 Federated Conference on Computer Science and Information Systems, volume 15 of Annals of Computer Science and Information Systems, pages 67\u201372. IEEE, 2018. doi:10.15439\/2018F88.10.15439\/2018F88","DOI":"10.15439\/2018F88"}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2020-0012","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T13:37:43Z","timestamp":1777383463000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2020-0012"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,7,1]]},"references-count":10,"journal-issue":{"issue":"2","published-online":{"date-parts":[[2021,1,9]]},"published-print":{"date-parts":[[2020,7,1]]}},"alternative-id":["10.2478\/forma-2020-0012"],"URL":"https:\/\/doi.org\/10.2478\/forma-2020-0012","relation":{},"ISSN":["1898-9934","1426-2630"],"issn-type":[{"value":"1898-9934","type":"electronic"},{"value":"1426-2630","type":"print"}],"subject":[],"published":{"date-parts":[[2020,7,1]]}}}