{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T11:04:59Z","timestamp":1774868699059,"version":"3.50.1"},"reference-count":13,"publisher":"Walter de Gruyter GmbH","issue":"1","license":[{"start":{"date-parts":[[2025,9,1]],"date-time":"2025-09-01T00:00:00Z","timestamp":1756684800000},"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":[[2025,9,1]]},"abstract":"<jats:title>Summary<\/jats:title>\n                  <jats:p>\n                    This article initiates a series devoted to the formalization of the Fundamental Theorem of Galois Theory. It presents several preliminaries required for the formal development of Galois theory. In particular, as a main result, we define the lattice of intermediate fields of an extension\n                    <jats:italic>E\/F<\/jats:italic>\n                    ; we also treat sets of functions, groups, and intermediate fields in order to provide the necessary cluster registrations that enable effective Mizar automation.\n                  <\/jats:p>","DOI":"10.2478\/forma-2025-0013","type":"journal-article","created":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T16:26:23Z","timestamp":1767975983000},"page":"165-174","source":"Crossref","is-referenced-by-count":1,"title":["The Lattice of Intermediate Fields and Other Preliminaries to Galois Theory"],"prefix":"10.2478","volume":"33","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"}]},{"given":"Agnieszka","family":"Rowi\u0144ska-Schwarzweller","sequence":"additional","affiliation":[{"name":"Institute of Informatics , University of Gda\u0144sk , Poland"}]}],"member":"374","published-online":{"date-parts":[[2025,12,31]]},"reference":[{"key":"2026033010152214184_j_forma-2025-0013_ref_001","doi-asserted-by":"crossref","unstructured":"Grzegorz Bancerek and Piotr Rudnicki. A Compendium of Continuous Lattices in Mizar. Journal of Automated Reasoning, 29(3\u20134):189\u2013224, 2002. doi:10.1023\/A:1021966832558.","DOI":"10.1023\/A:1021966832558"},{"key":"2026033010152214184_j_forma-2025-0013_ref_002","unstructured":"Garrett Birkho . Lattice Theory. Providence, Rhode Island, New York, 1967."},{"key":"2026033010152214184_j_forma-2025-0013_ref_003","unstructured":"David S. Dummit and Richard M. Foote. Abstract Algebra. Wiley and Sons, third edition, 2004."},{"key":"2026033010152214184_j_forma-2025-0013_ref_004","doi-asserted-by":"crossref","unstructured":"Adam Grabowski. Mechanizing complemented lattices within Mizar system. Journal of Automated Reasoning, 55:211\u2013221, 2015. doi:10.1007\/s10817-015-9333-5.","DOI":"10.1007\/s10817-015-9333-5"},{"key":"2026033010152214184_j_forma-2025-0013_ref_005","doi-asserted-by":"crossref","unstructured":"Adam Grabowski, Artur Korni\u0142owicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191\u2013198, 2015. doi:10.1007\/s10817-015-9345-1.","DOI":"10.1007\/s10817-015-9345-1"},{"key":"2026033010152214184_j_forma-2025-0013_ref_006","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":"2026033010152214184_j_forma-2025-0013_ref_007","doi-asserted-by":"crossref","unstructured":"George Gr\u00e4tzer. Lattice Theory: Foundation. Birkh\u00e4user, 2011.","DOI":"10.1007\/978-3-0348-0018-1"},{"key":"2026033010152214184_j_forma-2025-0013_ref_008","unstructured":"I. Martin Isaacs. Algebra: A Graduate Course. Wadsworth Inc., 1994."},{"key":"2026033010152214184_j_forma-2025-0013_ref_009","unstructured":"Serge Lang. Algebra (Revised Third Edition). Springer Verlag, 2002."},{"key":"2026033010152214184_j_forma-2025-0013_ref_010","unstructured":"Knut Radbruch. Algebra I. Lecture Notes, University of Kaiserslautern, Germany, 1991."},{"key":"2026033010152214184_j_forma-2025-0013_ref_011","doi-asserted-by":"crossref","unstructured":"Christoph Schwarzweller and Agnieszka Rowi\u0144ska-Schwarzweller. Simple extensions. Formalized Mathematics, 31(1):287\u2013298, 2023. doi:10.2478\/forma-2023-0023.","DOI":"10.2478\/forma-2023-0023"},{"key":"2026033010152214184_j_forma-2025-0013_ref_012","doi-asserted-by":"crossref","unstructured":"Ian Stewart. Galois Theory. Chapman and Hall\/CRC, fourth edition, 2015.","DOI":"10.1201\/b18187"},{"key":"2026033010152214184_j_forma-2025-0013_ref_013","doi-asserted-by":"crossref","unstructured":"Steven H. Weintraub. Galois Theory. Springer-Verlag, second edition, 2009.","DOI":"10.1007\/978-0-387-87575-0"}],"container-title":["Formalized Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.sciendo.com\/pdf\/10.2478\/forma-2025-0013","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T10:15:57Z","timestamp":1774865757000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.sciendo.com\/article\/10.2478\/forma-2025-0013"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,1]]},"references-count":13,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2025,12,31]]},"published-print":{"date-parts":[[2025,9,1]]}},"alternative-id":["10.2478\/forma-2025-0013"],"URL":"https:\/\/doi.org\/10.2478\/forma-2025-0013","relation":{},"ISSN":["1898-9934"],"issn-type":[{"value":"1898-9934","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,9,1]]}}}