35.1. Introduction🔗

HexPermGroup computes with groups of permutations of {0, …, n - 1} given by generators. It finds the order of such a group, its orbits and point stabilizers, decides whether a permutation belongs to it and if so writes the permutation as a word in the generators, and computes cosets, block systems, derived series and wreath products.

Its companion HexPermGroupTheory uses these computations to prove theorems about subgroups of Equiv.Perm (Fin n). For example, the Mathieu group M11 is generated by an 11-cycle and a product of two 4-cycles, and the perm_group tactic proves that it has order 7920:

example : Nat.card (Subgroup.closure
    ({c[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10],
      c[2, 6, 10, 7] * c[3, 9, 4, 5]} :
      Set (Equiv.Perm (Fin 11)))) = 7920 := by⊢ Nat.card
    ↥(Subgroup.closure
        {(↑[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10]).formPerm ⋯, (↑[2, 6, 10, 7]).formPerm ⋯ * (↑[3, 9, 4, 5]).formPerm ⋯}) =
  7920
  perm_groupAll goals completed! 🐙

The same tactic proves that a given permutation does or does not lie in such a subgroup, and that a list of permutations generates the whole symmetric group; see The Mathlib correspondence.

HexPermGroup itself does not depend on Mathlib. Import it for computation and for perm_group proofs about Hex permutations. Import HexPermGroupTheory for the extension and the theorems that translate its results into statements about Equiv.Perm (Fin n).