@[instance_reducible]

instance Hex.PermGroup.instGroupElement_hexPermGroupTheory {n : ℕ} (G : Group n) : _root_.Group (Element G)

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.PermGroup.Group.contains_spec {n : ℕ} (G : Group n) (p : Perm n) : G.contains p = true ↔ p.toEquiv ∈ closure G.generators

Membership and exact order of a checked computational group agree with its Mathlib subgroup, using the original generator presentation.

theorem Hex.PermGroup.Group.order_card {n : ℕ} (G : Group n) : G.order = Nat.card ↥(closure G.generators)

theorem Hex.PermGroup.Group.ofGenerators_spec {n : ℕ} (S : Array (Perm n)) : (∀ (p : Perm n), (ofGenerators S).contains p = true ↔ p.toEquiv ∈ closure S) ∧ (ofGenerators S).order = Nat.card ↥(closure S)

The deterministic constructor has exact Mathlib membership and cardinality for every input, with no assumed group order or successful search hypothesis.

def Hex.PermGroup.Element.equiv {n : ℕ} (G : Group n) : Element G ≃* ↥(closure G.generators)

Elements correspond by their permutation values, preserving multiplication.

Equations

• One or more equations did not get rendered due to their size.