{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,15]],"date-time":"2026-06-15T00:20:43Z","timestamp":1781482843853,"version":"3.54.1"},"reference-count":7,"publisher":"Walter de Gruyter GmbH","issue":"3","license":[{"start":{"date-parts":[[2021,9,1]],"date-time":"2021-09-01T00:00:00Z","timestamp":1630454400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,9,1]]},"abstract":"\n Summary<\/jats:bold>\n . In this article we further develop field theory in Mizar [1], [2]: we prove existence and uniqueness of splitting fields. We define the splitting field of a polynomial\n p<\/jats:italic>\n \u2208\n F<\/jats:italic>\n [\n X<\/jats:italic>\n ] as the smallest field extension of\n F<\/jats:italic>\n , in which\n p<\/jats:italic>\n splits into linear factors. From this follows, that for a splitting field\n E<\/jats:italic>\n of\n p<\/jats:italic>\n we have\n E<\/jats:italic>\n =\n F<\/jats:italic>\n (\n A<\/jats:italic>\n ) where\n A<\/jats:italic>\n is the set of\n p<\/jats:italic>\n \u2019s roots. Splitting fields are unique, however, only up to isomorphisms; to be more precise up to\n F<\/jats:italic>\n -isomorphims i.e. isomorphisms\n i<\/jats:italic>\n with\n \n i|\n F<\/jats:sub>\n <\/jats:italic>\n = Id\n \n F<\/jats:sub>\n <\/jats:italic>\n . We prove that two splitting fields of\n p<\/jats:italic>\n \u2208\n F<\/jats:italic>\n [\n X<\/jats:italic>\n ] are\n F<\/jats:italic>\n -isomorphic using the well-known technique [4], [3] of extending isomorphisms from\n F<\/jats:italic>\n 1<\/jats:sub>\n \u2192\n F<\/jats:italic>\n 2<\/jats:sub>\n to\n F<\/jats:italic>\n 1<\/jats:sub>\n (\n a<\/jats:italic>\n ) \u2192\n F<\/jats:italic>\n 2<\/jats:sub>\n (\n b<\/jats:italic>\n ) for\n a<\/jats:italic>\n and\n b<\/jats:italic>\n being algebraic over\n F<\/jats:italic>\n 1<\/jats:sub>\n and\n F<\/jats:italic>\n 2<\/jats:sub>\n , respectively.\n <\/jats:p>","DOI":"10.2478\/forma-2021-0013","type":"journal-article","created":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T01:56:04Z","timestamp":1641434164000},"page":"129-139","source":"Crossref","is-referenced-by-count":4,"title":["Splitting Fields"],"prefix":"10.2478","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9587-8737","authenticated-orcid":false,"given":"Christoph","family":"Schwarzweller","sequence":"first","affiliation":[{"name":"Institute of Informatics University of Gda\u0144sk Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"374","published-online":{"date-parts":[[2021,12,30]]},"reference":[{"key":"2026042801422759484_j_forma-2021-0013_ref_1","doi-asserted-by":"crossref","unstructured":"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":"2026042801422759484_j_forma-2021-0013_ref_2","unstructured":"Adam Grabowski and Christoph Schwarzweller. Translating mathematical vernacular into knowledge repositories. In Michael Kohlhase, editor, Mathematical Knowledge Management, volume 3863 of Lecture Notes in Computer Science, pages 49\u201364. Springer, 2006. doi:https:\/\/doi.org\/10.1007\/11618027 4. 4th International Conference on Mathematical Knowledge Management, Bremen, Germany, MKM 2005, July 15\u201317, 2005, Revised Selected Papers."},{"key":"2026042801422759484_j_forma-2021-0013_ref_3","unstructured":"Serge Lang. Algebra. Springer Verlag, 2002 (Revised Third Edition)."},{"key":"2026042801422759484_j_forma-2021-0013_ref_4","unstructured":"Knut Radbruch. Algebra I. Lecture Notes, University of Kaiserslautern, Germany, 1991."},{"key":"2026042801422759484_j_forma-2021-0013_ref_5","doi-asserted-by":"crossref","unstructured":"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":"2026042801422759484_j_forma-2021-0013_ref_6","doi-asserted-by":"crossref","unstructured":"Christoph Schwarzweller. Ring and field adjunctions, algebraic elements and minimal polynomials. Formalized Mathematics, 28(3):251\u2013261, 2020. doi:10.2478\/forma-2020-0022.10.2478\/forma-2020-0022","DOI":"10.2478\/forma-2020-0022"},{"key":"2026042801422759484_j_forma-2021-0013_ref_7","doi-asserted-by":"crossref","unstructured":"Christoph Schwarzweller, Artur Korni\u0142owicz, and Agnieszka Rowi\u0144ska-Schwarzweller. Some algebraic properties of polynomial rings. Formalized Mathematics, 24(3):227\u2013237, 2016. doi:10.1515\/forma-2016-0019.10.1515\/forma-2016-0019","DOI":"10.1515\/forma-2016-0019"}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2021-0013","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T14:09:00Z","timestamp":1777385340000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2021-0013"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,1]]},"references-count":7,"journal-issue":{"issue":"3","published-online":{"date-parts":[[2021,12,30]]},"published-print":{"date-parts":[[2021,9,1]]}},"alternative-id":["10.2478\/forma-2021-0013"],"URL":"https:\/\/doi.org\/10.2478\/forma-2021-0013","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,9,1]]}}}