Harrison, J. A Formalized Proof of Dirichlet’s Theorem on Primes in Arithmetic Progression. JFR 2009, 2, 63-83.