inductive Hex.PermGroup.Generated {n : Nat} (S : Array (Perm n)) : Perm n → Prop

Membership in the subgroup generated by the original input array.

• id {n : Nat} {S : Array (Perm n)} : Generated S (Perm.id n)
• generator {n : Nat} {S : Array (Perm n)} {p : Perm n} : p ∈ S → Generated S p
• comp {n : Nat} {S : Array (Perm n)} {p q : Perm n} : Generated S p → Generated S q → Generated S (p.comp q)
• inv {n : Nat} {S : Array (Perm n)} {p : Perm n} : Generated S p → Generated S p.inv

theorem Hex.PermGroup.Generated.lift {n : Nat} {S : Array (Perm n)} {P : Perm n → Prop} (hi : P (Perm.id n)) (hs : ∀ (p : Perm n), p ∈ S → P p) (hc : ∀ (p q : Perm n), P p → P q → P (p.comp q)) (hv : ∀ (p : Perm n), P p → P p.inv) {p : Perm n} (h : Generated S p) : P p

A predicate closed under the group operations contains the generated subgroup whenever it contains the input generators.

theorem Hex.PermGroup.Generated.mono {n : Nat} {S T : Array (Perm n)} (h : ∀ (p : Perm n), p ∈ S → Generated T p) {p : Perm n} (hp : Generated S p) : Generated T p

Replacing each generator by a word in another array preserves membership.

def Hex.PermGroup.GeneratesAll {n : Nat} (S : Array (Perm n)) : Prop

Every permutation of the declared degree is generated by S.

Equations

• Hex.PermGroup.GeneratesAll S = ∀ (p : Hex.Perm n), Hex.PermGroup.Generated S p