# Lehmer's Theorem

 Title: Lehmer's Theorem Authors: Simon Wimmer and Lars Noschinski Submission date: 2013-07-22 Abstract: 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. BibTeX: @article{Lehmer-AFP, author = {Simon Wimmer and Lars Noschinski}, title = {Lehmer's Theorem}, journal = {Archive of Formal Proofs}, month = jul, year = 2013, note = {\url{http://isa-afp.org/entries/Lehmer.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Used by: Pratt_Certificate