Classification of Finite Fields with Applications

被引：0

作者：

Hing-Lun Chan

Michael Norrish

机构：

[1] Australian National University,

[2] Canberra Research Laboratory,undefined

[3] Data61,undefined

来源：

Journal of Automated Reasoning | 2019年 / 63卷

关键词：

Monoid; Group; Ring; Field; Finite field; Subfield; Quotient field; Extension field; Isomorphism; Minimal polynomials; Cyclotomic polynomials; Primitives; Existence; Uniqueness; Theorem proving; Formalisation; HOL4;

D O I：

暂无

中图分类号：

学科分类号：

摘要：

We present a formalisation of the theory of finite fields, from basic axioms to their classification, both existence and uniqueness, in HOL4 using the notion of subfields. The tools developed are applied to the characterisation of subfields of finite fields, and to the cyclotomic factorisation of polynomials of the form [inline-graphic not available: see fulltext], with coefficients over a finite fields.

引用

页码：667 / 693

页数：26

共 12 条

[1]

Arneson B(2003)Witt’s proof of the Wedderburn theorem J. Formaliz. Math. 12 69-75

[2]

Baaz M(2003)Primitive roots of unity and cyclotomic polynomials J. Formaliz. Math 12 59-67

[3]

Rudnicki P(2008)A page in number theory J. Formaliz. Reason. 1 1-23

[4]

Arneson B(2013)A string of pearls: proofs of Fermat’s little theorem J. Formaliz. Reason. 6 63-87

[5]

Rudnicki P(2013)Formalization of definitions and theorems related to an elliptic curve over a finite prime field by using Mizar J. Automat. Reason. 50 161-172

[6]

Asperti A(undefined)undefined undefined undefined undefined-undefined

[7]

Armentano C(undefined)undefined undefined undefined undefined-undefined

[8]

Chan HL(undefined)undefined undefined undefined undefined-undefined

[9]

Norrish M(undefined)undefined undefined undefined undefined-undefined

[10]

Futa Yuichi(undefined)undefined undefined undefined undefined-undefined

← 1 2 →