This is an open-source project that formalises in the Lean theorem prover the classification of the groups of order p * q where p and q are prime numbers, using mathlib.
The main theorems are in Main.lean.
Also formalised as part of the project are some key properties of semidirect products of groups and a number of other group-theoretic results.
The authors are
The following pull requests (PRs) to mathlib and its dependencies were necessitated or inspired by this project. Further PRs will be made in due course.
- leanprover/lean4#4037: Added
dite_some_none_eq_noneanddite_some_none_eq_someto the moduleInit.ByCases. - leanprover-community/mathlib4#14097: Added
toAdd_eq_zeroandtoMul_eq_oneto the moduleMathlib.Algebra.Group.TypeTags. - leanprover-community/mathlib4#14104 and leanprover-community/mathlib4#14154: Added
Prod.orderOf_mkto the moduleMathlib.GroupTheory.OrderOfElement. - leanprover-community/mathlib4#14365: Added lemmas on sufficient conditions for two
Sets orSubgroups to be equal. - leanprover-community/mathlib4#17057: Added instances of
Finite,Fintype,DecidableEqforMulEquiv.
The source code of this project is distributed under the terms of the Apache License 2.0. See LICENSE for more details.