Harrison, J. 2009. A formalized proof of Dirichlet’s theorem on primes in arithmetic progression. Journal of Formalized Reasoning. 2, 1 (Jan. 2009), 63–83. DOI:https://doi.org/10.6092/issn.1972-5787/1558.