Finite Fields

被引：0
作者：
Schwarzweller, Christoph [1 ]
机构：
[1] Univ Gdansk, Inst Informat, Gdansk, Poland
来源：
FORMALIZED MATHEMATICS | 2024年 / 32卷 / 01期
关键词：
finite field; splitting field; Galois field;
D O I：
10.2478/forma-2024-0024
中图分类号：
O1 [数学];
学科分类号：
0701 ; 070101 ;
摘要：
We continue the formalization of field theory in Mizar. Here we prove existence and uniqueness of finite fields by constructing the splitting field of the polynomial X(pn) -X over the prime field of a field with characteristic p. We also define the Frobenius morphism and show that the automorphisms of a field with pn elements are exactly the powers 0, . . ., n - 1 of the Frobenius morphism, that is the automorphism group is generated by the Frobenius morphism.
引用
收藏
页码：289 / 302
页数：14
相关论文
共 13 条
  • [1] The Role of the Mizar Mathematical Library for Interactive Proof Development in Mizar
    Bancerek, Grzegorz
    Bylinski, Czeslaw
    Grabowski, Adam
    Kornilowicz, Artur
    Matuszewski, Roman
    Naumowicz, Adam
    Pak, Karol
    [J]. JOURNAL OF AUTOMATED REASONING, 2018, 61 (1-4) : 9 - 32
  • [2] Mizar: State-of-the-Art and Beyond
    Bancerek, Grzegorz
    Bylinski, Czeslaw
    Grabowski, Adam
    Kornilowicz, Artur
    Matuszewski, Roman
    Naumowicz, Adam
    Pak, Karol
    Urban, Josef
    [J]. INTELLIGENT COMPUTER MATHEMATICS, CICM 2015, 2015, 9150 : 261 - 279
  • [3] On Algebraic Hierarchies in Mathematical Repository of Mizar
    Grabowski, Adam
    Kornilowicz, Artur
    Schwarzweller, Christoph
    [J]. PROCEEDINGS OF THE 2016 FEDERATED CONFERENCE ON COMPUTER SCIENCE AND INFORMATION SYSTEMS (FEDCSIS), 2016, 8 : 363 - 371
  • [4] Equality in Computer Proof-Assistants
    Grabowski, Adam
    Kornilowicz, Artur
    Schwarzweller, Christoph
    [J]. PROCEEDINGS OF THE 2015 FEDERATED CONFERENCE ON COMPUTER SCIENCE AND INFORMATION SYSTEMS, 2015, 5 : 45 - 54
  • [5] Jacobson N., 1985, Basic Algebra, VI
  • [6] Karayel Emin, 2022, Archive of Formal Proofs
  • [7] The First Isomorphism Theorem and Other Properties of Rings
    Kornilowicz, Artur
    Schwarzweller, Christoph
    [J]. FORMALIZED MATHEMATICS, 2014, 22 (04): : 291 - 301
  • [8] Flexary connectives in Mizar
    Kornilowicz, Artur
    [J]. COMPUTER LANGUAGES SYSTEMS & STRUCTURES, 2015, 44 : 238 - 250
  • [9] Lang S., 2002, Graduate Texts in Mathematics, V211
  • [10] Radbruch Knut, 1991, Lecture Notes
12