Harrison, John. “A Formalized Proof of Dirichlet’s Theorem on Primes in Arithmetic Progression”. Journal of Formalized Reasoning 2, no. 1 (January 1, 2009): 63–83. Accessed April 26, 2024. https://jfr.unibo.it/article/view/1558.