Classifying the groups of order $p q$ in Lean
Logic in Computer Science
2025-01-23 v2 Group Theory
Abstract
This note discusses our formalisation in Lean of the classification of the groups of order for (not necessarily distinct) prime numbers and , together with various intermediate results such as the characterisation of internal direct and semidirect products.
Cite
@article{arxiv.2501.09769,
title = {Classifying the groups of order $p q$ in Lean},
author = {Scott Harper and Peiran Wu},
journal= {arXiv preprint arXiv:2501.09769},
year = {2025}
}