Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Finite Fields

Email Gateway (Jun 16 2022 at 07:14):

From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,

I’m happy to announce a new AFP entry:

Finite Fields
by Emin Karayel

This entry formalizes the classification of the finite fields (also called Galois fields):
For each prime power p^n there exists exactly one (up to isomorphisms) finite field of that
size and there are no other finite fields. The derivation includes a formalization of the
characteristic of rings, the Frobenius endomorphism, formal differentiation for polynomials
in HOL-Algebra and Gauss' formula for the number of monic irreducible polynomials over finite
fields:

1/n * sum_{d | n} mu(d) p^(n/d).

The proofs are based on the books from Ireland and Rosen, as well as, Lidl and Niederreiter.

Best,
René

Last updated: Jul 15 2022 at 23:21 UTC