No results found

order-pq

Lean formalisation of the classification of the groups of order `p * q` where `p` and `q` are prime numbers.

OrderPQ

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

Upstream PRs

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_none and dite_some_none_eq_some to the module Init.ByCases.
  • leanprover-community/mathlib4#14097: Added toAdd_eq_zero and toMul_eq_one to the module Mathlib.Algebra.Group.TypeTags.
  • leanprover-community/mathlib4#14104 and leanprover-community/mathlib4#14154: Added Prod.orderOf_mk to the module Mathlib.GroupTheory.OrderOfElement.
  • leanprover-community/mathlib4#14365: Added lemmas on sufficient conditions for two Sets or Subgroups to be equal.

License

The source code of this project is distributed under the terms of the Apache License 2.0. See LICENSE for more details.