← All papers
Classifying the groups of order $p q$ in Lean
cs.LO
Jan 16, 2025 · v1
TL;DR
Formalizes in Lean the classification of groups of order pq, with intermediate results on internal direct and semidirect products.
Abstract
This note discusses our formalisation in Lean of the classification of the groups of order $p q$ for (not necessarily distinct) prime numbers $p$ and $q$, together with various intermediate results such as the characterisation of internal direct and semidirect products.
Problem
The classification of groups of order pq for prime numbers p and q is a standard result in algebra, but it had not been formalized in Lean along with the necessary characterization of internal direct and semidirect products.
Approach
The authors formalize in Lean the classification of groups of order pq for not necessarily distinct primes p and q. The formalization includes intermediate results such as the characterization of internal direct and semidirect products, building on existing group theory infrastructure in mathlib.
Results
The classification theorem is fully formalized in Lean, covering all cases of groups of order pq including the direct and semidirect product characterizations needed for the proof.