Classification of finite fields with applications

DOI10.1007/S10817-018-9485-1MaRDI QIDQ2323448zbMATH OpenOpenAlexFDO

Authors Michael Norrish, Hing-Lun Chan

Publication date 2 September 2019

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-018-9485-1

zbMATH Keywords

cyclotomic polynomialsexistenceextension fieldfieldfinite fieldformalisationgroupHOL4isomorphismminimal polynomialsmonoidprimitivesquotient fieldringsubfieldtheorem provinguniqueness

Mathematics Subject Classification ID

Finite fields and commutative rings (number-theoretic aspects) (11Txx) Finite fields (field-theoretic aspects) (12E20) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Finding Isomorphisms Between Finite Fields
• scientific article; zbMATH DE number 4152523
• Characteristic of rings. Prime fields
• scientific article; zbMATH DE number 3882549
• Finite fields.

Cites work

• A classical introduction to Galois theory
• A course in error-correcting codes.
• A formal library for elliptic curves in the Coq proof assistant
• A machine-checked proof of the odd order theorem
• A string of pearls: proofs of Fermat's little theorem
• A verified implementation of the Berlekamp-Zassenhaus factorization algorithm
• Advanced modern algebra
• Algebraic numbers in Isabelle/HOL
• Canonical structures for the working Coq user
• Construction of real algebraic numbers in Coq
• Formalization of definitions and theorems related to an elliptic curve over a finite prime field by using Mizar
• scientific article; zbMATH DE number 5995471 (Why is no real title available?)
• scientific article; zbMATH DE number 3882553 (Why is no real title available?)
• scientific article; zbMATH DE number 5587007 (Why is no real title available?)
• scientific article; zbMATH DE number 4023423 (Why is no real title available?)
• scientific article; zbMATH DE number 4083539 (Why is no real title available?)
• scientific article; zbMATH DE number 47996 (Why is no real title available?)
• scientific article; zbMATH DE number 54194 (Why is no real title available?)
• scientific article; zbMATH DE number 734977 (Why is no real title available?)
• scientific article; zbMATH DE number 854560 (Why is no real title available?)
• scientific article; zbMATH DE number 928753 (Why is no real title available?)
• Linear algebra done right
• Mechanisation of AKS algorithm. I. The main theorem
• Primality Proving with Elliptic Curves
• Röver's simple group is of type \(F_\infty\)
• The mathematics of coding theory. Information, compression, error correction and finite fields.
• Verification of the Miller-Rabin probabilistic primality test.

Cited in

(3)

• Mechanisation of the AKS algorithm
• Generalizations of complete mappings of finite fields and some applications
• Characteristic of rings. Prime fields

Describes a project that uses

Uses Software

• Isabelle
• Berlekamp Zassenhaus
• Isabelle/HOL
• Mizar
• Mathematical Components
• Coq
• HOL
• finfield.v
• GitHub

This page was built for publication: Classification of finite fields with applications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2323448)