Classifying the groups of order $pq$ in Lean

Scott Harper, Peiran Wu

This note discusses our formalisation in Lean of the classification of the groups of order $pq$ for (not necessarily distinct) prime numbers $p$ and $q$, together with various int…