Lehmer's Theorem

Simon Wimmer 📧 and Lars Noschinski 🌐

July 22, 2013

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


In 1927, Lehmer presented criterions for primality, based on the converse of Fermat's litte theorem. This work formalizes the second criterion from Lehmer's paper, a necessary and sufficient condition for primality.

As a side product we formalize some properties of Euler's phi-function, the notion of the order of an element of a group, and the cyclicity of the multiplicative group of a finite field.


BSD License


Session Lehmer