Classification of Finite Fields with Applications

Hing Lun Chan; Michael Norrish

doi:10.1007/s10817-018-9485-1

Classification of Finite Fields with Applications

Hing Lun Chan^*, Michael Norrish

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

1 Citation (Scopus)

Abstract

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 [InlineEquation not available: see fulltext.], with coefficients over a finite fields.

Original language	English
Pages (from-to)	667-693
Number of pages	27
Journal	Journal of Automated Reasoning
Volume	63
Issue number	3
DOIs	https://doi.org/10.1007/s10817-018-9485-1
Publication status	Published - 15 Oct 2019

Access to Document

10.1007/s10817-018-9485-1

Cite this

@article{db226b33c53f48b5a11cedf1062bb272,

title = "Classification of Finite Fields with Applications",

abstract = "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 [InlineEquation not available: see fulltext.], with coefficients over a finite fields.",

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

author = "Chan, {Hing Lun} and Michael Norrish",

note = "Publisher Copyright: {\textcopyright} 2018, Springer Nature B.V.",

year = "2019",

month = oct,

day = "15",

doi = "10.1007/s10817-018-9485-1",

language = "English",

volume = "63",

pages = "667--693",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "3",

}

TY - JOUR

T1 - Classification of Finite Fields with Applications

AU - Chan, Hing Lun

AU - Norrish, Michael

PY - 2019/10/15

Y1 - 2019/10/15

N2 - 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 [InlineEquation not available: see fulltext.], with coefficients over a finite fields.

AB - 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 [InlineEquation not available: see fulltext.], with coefficients over a finite fields.

KW - Cyclotomic polynomials

KW - Existence

KW - Extension field

KW - Field

KW - Finite field

KW - Formalisation

KW - Group

KW - HOL4

KW - Isomorphism

KW - Minimal polynomials

KW - Monoid

KW - Primitives

KW - Quotient field

KW - Ring

KW - Subfield

KW - Theorem proving

KW - Uniqueness

UR - http://www.scopus.com/inward/record.url?scp=85055868702&partnerID=8YFLogxK

U2 - 10.1007/s10817-018-9485-1

DO - 10.1007/s10817-018-9485-1

M3 - Article

SN - 0168-7433

VL - 63

SP - 667

EP - 693

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 3

ER -

Classification of Finite Fields with Applications

Abstract

Access to Document

Other files and links

Fingerprint

Cite this