{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T18:08:35Z","timestamp":1777486115754,"version":"3.51.4"},"reference-count":13,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2022,4,1]],"date-time":"2022-04-01T00:00:00Z","timestamp":1648771200000},"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":[[2022,4,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats:p>\n                    In [11] the existence (and uniqueness) of splitting fields has been formalized. In this article we apply this result by providing splitting fields for the polynomials\n                    <jats:italic>X<\/jats:italic>\n                    <jats:sup>2<\/jats:sup>\n                    \u2212 2,\n                    <jats:italic>X<\/jats:italic>\n                    <jats:sup>3<\/jats:sup>\n                    \u2212 1,\n                    <jats:italic>X<\/jats:italic>\n                    <jats:sup>2<\/jats:sup>\n                    +\n                    <jats:italic>X<\/jats:italic>\n                    + 1 and\n                    <jats:italic>X<\/jats:italic>\n                    <jats:sup>3<\/jats:sup>\n                    \u2212 2 over\n                    <jats:italic>Q<\/jats:italic>\n                    using the Mizar [2], [1] formalism. We also compute the degrees and bases for these splitting fields, which requires some additional registrations to adopt types properly.\n                  <\/jats:p>\n                  <jats:p>\n                    The main result, however, is that the polynomial\n                    <jats:italic>X<\/jats:italic>\n                    <jats:sup>3<\/jats:sup>\n                    \u2212 2 does not split over\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"graphic\/j_forma-2022-0003_eq_001.png\"\/>\n                        <m:math xmlns:m=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                          <m:mrow>\n                            <m:mi>\ud835\udcac<\/m:mi>\n                            <m:mrow>\n                              <m:mo>(<\/m:mo>\n                              <m:mrow>\n                                <m:mroot>\n                                  <m:mn>2<\/m:mn>\n                                  <m:mn>3<\/m:mn>\n                                <\/m:mroot>\n                              <\/m:mrow>\n                              <m:mo>)<\/m:mo>\n                            <\/m:mrow>\n                          <\/m:mrow>\n                        <\/m:math>\n                        <jats:tex-math>\\mathcal{Q}\\left( {\\root 3 \\of 2 } \\right)<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    . Because\n                    <jats:italic>X<\/jats:italic>\n                    <jats:sup>3<\/jats:sup>\n                    \u2212 2 obviously has a root over\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"graphic\/j_forma-2022-0003_eq_002.png\"\/>\n                        <m:math xmlns:m=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                          <m:mrow>\n                            <m:mi>\ud835\udcac<\/m:mi>\n                            <m:mrow>\n                              <m:mo>(<\/m:mo>\n                              <m:mrow>\n                                <m:mroot>\n                                  <m:mn>2<\/m:mn>\n                                  <m:mn>3<\/m:mn>\n                                <\/m:mroot>\n                              <\/m:mrow>\n                              <m:mo>)<\/m:mo>\n                            <\/m:mrow>\n                          <\/m:mrow>\n                        <\/m:math>\n                        <jats:tex-math>\\mathcal{Q}\\left( {\\root 3 \\of 2 } \\right)<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    this shows that the field extension\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" xlink:href=\"graphic\/j_forma-2022-0003_eq_003.png\"\/>\n                        <m:math xmlns:m=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                          <m:mrow>\n                            <m:mi>\ud835\udcac<\/m:mi>\n                            <m:mrow>\n                              <m:mo>(<\/m:mo>\n                              <m:mrow>\n                                <m:mroot>\n                                  <m:mn>2<\/m:mn>\n                                  <m:mn>3<\/m:mn>\n                                <\/m:mroot>\n                              <\/m:mrow>\n                              <m:mo>)<\/m:mo>\n                            <\/m:mrow>\n                          <\/m:mrow>\n                        <\/m:math>\n                        <jats:tex-math>\\mathcal{Q}\\left( {\\root 3 \\of 2 } \\right)<\/jats:tex-math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    is not normal over\n                    <jats:italic>Q<\/jats:italic>\n                    [3], [4], [5] and [7].\n                  <\/jats:p>","DOI":"10.2478\/forma-2022-0003","type":"journal-article","created":{"date-parts":[[2022,12,21]],"date-time":"2022-12-21T05:26:15Z","timestamp":1671600375000},"page":"23-30","source":"Crossref","is-referenced-by-count":1,"title":["Splitting Fields for the Rational Polynomials X\n                    <sup>2<\/sup>\n                    \u22122, X\n                    <sup>2<\/sup>\n                    +X+1, X\n                    <sup>3<\/sup>\n                    \u22121, and X\n                    <sup>3<\/sup>\n                    \u22122"],"prefix":"10.2478","volume":"30","author":[{"given":"Christoph","family":"Schwarzweller","sequence":"first","affiliation":[{"name":"Institute of Informatics , University of Gda\u0144sk , Poland"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sara","family":"Burgoa","sequence":"additional","affiliation":[{"name":"Weston, Florida United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"374","published-online":{"date-parts":[[2022,12,21]]},"reference":[{"key":"2026042801431125853_j_forma-2022-0003_ref_001","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-817.","DOI":"10.1007\/978-3-319-20615-8_17"},{"key":"2026042801431125853_j_forma-2022-0003_ref_002","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.604425130069070","DOI":"10.1007\/s10817-017-9440-6"},{"key":"2026042801431125853_j_forma-2022-0003_ref_003","unstructured":"[3] Nathan Jacobson. Basic Algebra I. Dover Books on Mathematics, 1985."},{"key":"2026042801431125853_j_forma-2022-0003_ref_004","unstructured":"[4] Serge Lang. Algebra. Springer Verlag, 2002 (Revised Third Edition)."},{"key":"2026042801431125853_j_forma-2022-0003_ref_005","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":"2026042801431125853_j_forma-2022-0003_ref_006","unstructured":"[6] Anna Justyna Milewska. The field of complex numbers. Formalized Mathematics, 9(2): 265\u2013269, 2001."},{"key":"2026042801431125853_j_forma-2022-0003_ref_007","unstructured":"[7] Knut Radbruch. Algebra I. Lecture Notes, University of Kaiserslautern, Germany, 1991."},{"key":"2026042801431125853_j_forma-2022-0003_ref_008","doi-asserted-by":"crossref","unstructured":"[8] Christoph Schwarzweller. Field extensions and Kronecker\u2019s construction. Formalized Mathematics, 27(3):229\u2013235, 2019. doi:10.2478\/forma-2019-0022.","DOI":"10.2478\/forma-2019-0022"},{"key":"2026042801431125853_j_forma-2022-0003_ref_009","doi-asserted-by":"crossref","unstructured":"[9] 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":"2026042801431125853_j_forma-2022-0003_ref_010","doi-asserted-by":"crossref","unstructured":"[10] 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":"2026042801431125853_j_forma-2022-0003_ref_011","doi-asserted-by":"crossref","unstructured":"[11] Christoph Schwarzweller. Splitting fields. Formalized Mathematics, 29(3):129\u2013139, 2021. doi:10.2478\/forma-2021-0013.","DOI":"10.2478\/forma-2021-0013"},{"key":"2026042801431125853_j_forma-2022-0003_ref_012","doi-asserted-by":"crossref","unstructured":"[12] 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":"2026042801431125853_j_forma-2022-0003_ref_013","doi-asserted-by":"crossref","unstructured":"[13] Christoph Schwarzweller and Agnieszka Rowi\u0144ska-Schwarzweller. Algebraic extensions. Formalized Mathematics, 29(1):39\u201348, 2021. doi:10.2478\/forma-2021-0004.","DOI":"10.2478\/forma-2021-0004"}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/reference-global.com\/pdf\/10.2478\/forma-2022-0003","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T14:27:36Z","timestamp":1777386456000},"score":1,"resource":{"primary":{"URL":"https:\/\/reference-global.com\/article\/10.2478\/forma-2022-0003"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,1]]},"references-count":13,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2022,12,21]]},"published-print":{"date-parts":[[2022,4,1]]}},"alternative-id":["10.2478\/forma-2022-0003"],"URL":"https:\/\/doi.org\/10.2478\/forma-2022-0003","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,1]]}}}