J. Harrison, “A formalized proof of Dirichlet’s theorem on primes in arithmetic progression”, JFR, vol. 2, no. 1, pp. 63–83, Jan. 2009.