Lehmer's Theorem

Simon Wimmer 📧 and Lars Noschinski 🌐

July 22, 2013


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