def Hex.PermGroup.closure {n : ℕ} (S : Array (Perm n)) : Subgroup (Equiv.Perm (Fin n))

The mathematical subgroup generated by the converted original inputs.

Equations

• Hex.PermGroup.closure S = Subgroup.closure {e : Equiv.Perm (Fin n) | ∃ p ∈ S, p.toEquiv = e}

theorem Hex.PermGroup.generated_iff_mem {n : ℕ} {S : Array (Perm n)} {p : Perm n} : Generated S p ↔ p.toEquiv ∈ closure S

Generated-subgroup semantics agrees with Mathlib subgroup closure.

noncomputable def Hex.PermGroup.generatedEquiv {n : ℕ} (S : Array (Perm n)) : { p : Perm n // Generated S p } ≃ ↥(closure S)

Convert generated Hex permutations to Mathlib's closure, without changing which elements are counted.

Equations

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

theorem Hex.PermGroup.hasOrder_iff_card {n : ℕ} {S : Array (Perm n)} {N : ℕ} : HasOrder S N ↔ Nat.card ↥(closure S) = N

The Mathlib-free order predicate is exactly Mathlib's cardinality statement.

theorem Hex.PermGroup.setOf_mem_cons {α : Type} (a b : α) (l : List α) : {x : α | x ∈ a :: b :: l} = insert a {x : α | x ∈ b :: l}

theorem Hex.PermGroup.setOf_mem_singleton {α : Type} (a : α) : {x : α | x ∈ [a]} = {a}

theorem Hex.PermGroup.setOf_mem_nil {α : Type} : {x : α | x ∈ []} = ∅

theorem Hex.PermGroup.closure_ofEquiv {n : ℕ} (gs : List (Equiv.Perm (Fin n))) : closure (List.map Perm.ofEquiv gs).toArray = Subgroup.closure {x : Equiv.Perm (Fin n) | x ∈ gs}

theorem Hex.PermGroup.card_of_hasOrder {n : ℕ} {gs : List (Equiv.Perm (Fin n))} {N : ℕ} (h : HasOrder (List.map Perm.ofEquiv gs).toArray N) : Nat.card ↥(Subgroup.closure {x : Equiv.Perm (Fin n) | x ∈ gs}) = N

Translate a computational order proof for a closed generating list.

theorem Hex.PermGroup.mem_of_generated {n : ℕ} {gs : List (Equiv.Perm (Fin n))} {g : Equiv.Perm (Fin n)} (h : Generated (List.map Perm.ofEquiv gs).toArray (Perm.ofEquiv g)) : g ∈ Subgroup.closure {x : Equiv.Perm (Fin n) | x ∈ gs}

Translate computational generation for a closed generating list.

theorem Hex.PermGroup.not_mem_of_neg {n : ℕ} {gs : List (Equiv.Perm (Fin n))} {g : Equiv.Perm (Fin n)} (h : ¬Generated (List.map Perm.ofEquiv gs).toArray (Perm.ofEquiv g)) : g ∉ Subgroup.closure {x : Equiv.Perm (Fin n) | x ∈ gs}

theorem Hex.PermGroup.generatesAll_iff_eq_top {n : ℕ} {S : Array (Perm n)} : GeneratesAll S ↔ closure S = ⊤

Full generation corresponds directly to the top subgroup.

theorem Hex.PermGroup.eq_top_of_all {n : ℕ} {gs : List (Equiv.Perm (Fin n))} (h : GeneratesAll (List.map Perm.ofEquiv gs).toArray) : Subgroup.closure {x : Equiv.Perm (Fin n) | x ∈ gs} = ⊤

Translate full generation for a closed generating list.