theorem Hex.PermGroup.LeftCoset.eq_spec {n : ℕ} (H : Group n) (p q : Perm n) : mk H p = mk H q ↔ p.toEquiv • ↑(closure H.generators) = q.toEquiv • ↑(closure H.generators)

Computational coset equality agrees with Mathlib left cosets.

theorem Hex.PermGroup.Group.index_spec {n : ℕ} (G H : Group n) (h : H.IsSubgroup G) : G.index H h = (closure H.generators).relIndex (closure G.generators)

The exact division used by the executable API is Mathlib's relative index.

theorem Hex.PermGroup.LeftTransversal.cosets_spec {n : ℕ} {G H : Group n} (t : LeftTransversal G H) (h : H.IsSubgroup G) (p : Perm n) : (∃ (i : Fin t.reps.size), p.toEquiv ∈ (↑t.reps[↑i]).toEquiv • ↑(closure H.generators)) ↔ p.toEquiv ∈ closure G.generators

The returned cosets cover exactly the larger Mathlib subgroup.

theorem Hex.PermGroup.LeftTransversal.disjoint_spec {n : ℕ} {G H : Group n} (t : LeftTransversal G H) {i j : Fin t.reps.size} (hne : i ≠ j) : Disjoint ((↑t.reps[↑i]).toEquiv • ↑(closure H.generators)) ((↑t.reps[↑j]).toEquiv • ↑(closure H.generators))