Classifying the groups of order $pq$ in Lean

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 intermediate results such as the characterisation of internal direct and semidirect products.