{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,15]],"date-time":"2026-06-15T01:08:29Z","timestamp":1781485709897,"version":"3.54.1"},"reference-count":15,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2023,9,1]],"date-time":"2023-09-01T00:00:00Z","timestamp":1693526400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,9,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats:p>\n                    In this article we continue the formalization of field theory in Mizar. We introduce simple extensions: an extension\n                    <jats:italic>E<\/jats:italic>\n                    of\n                    <jats:italic>F<\/jats:italic>\n                    is simple if\n                    <jats:italic>E<\/jats:italic>\n                    is generated over\n                    <jats:italic>F<\/jats:italic>\n                    by a single element of\n                    <jats:italic>E<\/jats:italic>\n                    , that is\n                    <jats:italic>E<\/jats:italic>\n                    =\n                    <jats:italic>F<\/jats:italic>\n                    (\n                    <jats:italic>a<\/jats:italic>\n                    ) for some\n                    <jats:italic>a<\/jats:italic>\n                    \u2208\n                    <jats:italic>E<\/jats:italic>\n                    . First, we prove that a finite extension\n                    <jats:italic>E<\/jats:italic>\n                    of\n                    <jats:italic>F<\/jats:italic>\n                    is simple if and only if there are only finitely many intermediate fields between\n                    <jats:italic>E<\/jats:italic>\n                    and\n                    <jats:italic>F<\/jats:italic>\n                    [7]. Second, we show that finite extensions of a field\n                    <jats:italic>F<\/jats:italic>\n                    with characteristic 0 are always simple [1]. For this we had to prove, that irreducible polynomials over\n                    <jats:italic>F<\/jats:italic>\n                    have single roots only, which required extending results on divisibility and gcds of polynomials [14], [13] and formal derivation of polynomials [15].\n                  <\/jats:p>","DOI":"10.2478\/forma-2023-0023","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T10:21:58Z","timestamp":1704450118000},"page":"287-298","source":"Crossref","is-referenced-by-count":5,"title":["Simple Extensions"],"prefix":"10.2478","volume":"31","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"}]},{"given":"Agnieszka","family":"Rowi\u0144ska-Schwarzweller","sequence":"additional","affiliation":[{"name":"Institute of Informatics , University of Gda\u0144sk , Poland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"374","published-online":{"date-parts":[[2023,12,31]]},"reference":[{"key":"2026042801415043114_j_forma-2023-0023_ref_001","unstructured":"Andreas Gathmann. Einf\u00fchrung in die Algebra. Lecture Notes, University of Kaiserslautern, Germany, 2011."},{"key":"2026042801415043114_j_forma-2023-0023_ref_002","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:10.1007\/11618027 4. 4th International Conference on Mathematical Knowledge Management, Bremen, Germany, MKM 2005, July 15\u201317, 2005, Revised Selected Papers."},{"key":"2026042801415043114_j_forma-2023-0023_ref_003","unstructured":"Adam Grabowski, Artur Korni\u0142owicz, and Adam Naumowicz. Mizar in a nutshell. Journal of Formalized Reasoning, 3(2):153\u2013245, 2010."},{"key":"2026042801415043114_j_forma-2023-0023_ref_004","doi-asserted-by":"crossref","unstructured":"Adam Grabowski, Artur Korni\u0142owicz, and Christoph Schwarzweller. On algebraic hierarchies in mathematical repository of Mizar. In M. Ganzha, L. Maciaszek, and M. Paprzycki, editors, Proceedings of the 2016 Federated Conference on Computer Science and Information Systems (FedCSIS), volume 8 of Annals of Computer Science and Information Systems, pages 363\u2013371, 2016. doi:10.15439\/2016F520.","DOI":"10.15439\/2016F520"},{"key":"2026042801415043114_j_forma-2023-0023_ref_005","doi-asserted-by":"crossref","unstructured":"Artur Korni\u0142owicz. Flexary connectives in Mizar. Computer Languages, Systems & Structures, 44:238\u2013250, December 2015. doi:10.1016\/j.cl.2015.07.002.","DOI":"10.1016\/j.cl.2015.07.002"},{"key":"2026042801415043114_j_forma-2023-0023_ref_006","unstructured":"Serge Lang. Algebra. PWN, Warszawa, 1984."},{"key":"2026042801415043114_j_forma-2023-0023_ref_007","unstructured":"Serge Lang. Algebra. Springer Verlag, 2002 (Revised Third Edition)."},{"key":"2026042801415043114_j_forma-2023-0023_ref_008","doi-asserted-by":"crossref","unstructured":"Heinz L\u00fcneburg. Gruppen, Ringe, K\u00f6rper: Die grundlegenden Strukturen der Algebra. Oldenbourg Verlag, 1999.","DOI":"10.1524\/9783486599022"},{"key":"2026042801415043114_j_forma-2023-0023_ref_009","doi-asserted-by":"crossref","unstructured":"Christoph Schwarzweller. Normal extensions. Formalized Mathematics, 31(1):121\u2013130, 2023. doi:10.2478\/forma-2023-0011.","DOI":"10.2478\/forma-2023-0011"},{"key":"2026042801415043114_j_forma-2023-0023_ref_010","doi-asserted-by":"crossref","unstructured":"Christoph Schwarzweller. Renamings and a condition-free formalization of Kronecker\u2019s construction. Formalized Mathematics, 28(2):129\u2013135, 2020. doi:10.2478\/forma-2020-0012.","DOI":"10.2478\/forma-2020-0012"},{"key":"2026042801415043114_j_forma-2023-0023_ref_011","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.","DOI":"10.2478\/forma-2020-0022"},{"key":"2026042801415043114_j_forma-2023-0023_ref_012","doi-asserted-by":"crossref","unstructured":"Christoph Schwarzweller. Splitting fields. Formalized Mathematics, 29(3):129\u2013139, 2021. doi:10.2478\/forma-2021-0013.","DOI":"10.2478\/forma-2021-0013"},{"key":"2026042801415043114_j_forma-2023-0023_ref_013","doi-asserted-by":"crossref","unstructured":"Christoph Schwarzweller. On roots of polynomials and algebraically closed fields. Formalized Mathematics, 25(3):185\u2013195, 2017. doi:10.1515\/forma-2017-0018.","DOI":"10.1515\/forma-2017-0018"},{"key":"2026042801415043114_j_forma-2023-0023_ref_014","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.","DOI":"10.1515\/forma-2016-0019"},{"key":"2026042801415043114_j_forma-2023-0023_ref_015","doi-asserted-by":"crossref","unstructured":"Yasushige Watase. Derivation of commutative rings and the Leibniz formula for power of derivation. Formalized Mathematics, 29(1):1\u20138, 2021. doi:10.2478\/forma-2021-0001.","DOI":"10.2478\/forma-2021-0001"}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2023-0023","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T13:56:46Z","timestamp":1777384606000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2023-0023"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,1]]},"references-count":15,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2023,12,31]]},"published-print":{"date-parts":[[2023,9,1]]}},"alternative-id":["10.2478\/forma-2023-0023"],"URL":"https:\/\/doi.org\/10.2478\/forma-2023-0023","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,9,1]]}}}