Prime cyclic and alternating representatives

Definition

wilson_elementary_groups

by joe · Jul 22, 2026 · Mathlib c5ea003 (Lean v4.30.0)

classificationfinite-groupsgroup-theory

This module supplies the first concrete representatives in Wilson’s catalog. The prime-order cyclic entry with parameter $p$ is the additive group of $mathbb Z/pmathbb Z$ , presented multiplicatively. The alternating entry with degree $n$ is the even-permutation subgroup $A_nleq S_n$ .

The constructions exist for all natural-number parameters. Primality of $p$ and the restriction $ngeq5$ are imposed separately by the catalog admissibility predicate, so the definitions themselves do not assume finiteness or simplicity.

Definition code

import Definitions.Def_wilson_catalog_labels
import Mathlib.Data.ZMod.Basic
import Mathlib.GroupTheory.SpecificGroups.Alternating

namespace WilsonCatalog

/-- The cyclic group of order `p`, written multiplicatively.  Primality is an
admissibility condition on its catalog label, not part of this construction. -/
abbrev PrimeCyclicGroup (p : Nat) := Multiplicative (ZMod p)

/-- The alternating group on `degree` letters.  The bound `5 ≤ degree` is an
admissibility condition on its catalog label, not part of this construction. -/
abbrev AlternatingGroup (degree : Nat) := alternatingGroup (Fin degree)

end WilsonCatalog

Source

Robert A. Wilson, The Finite Simple Groups, Graduate Texts in Mathematics 251, Springer (2009), Chapter 1 and Chapter 2, pp. 1–39, https://doi.org/10.1007/978-1-84800-988-2

View graph