def Hex.PermGroup.Search.Normalizer.test {n : Nat} (H : Group n) (p : Perm n) : Bool

Check conjugates of original generators in both directions. This proves subgroup equality, including when the second group lies outside the ambient one.

Equations

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

theorem Hex.PermGroup.Search.Normalizer.preserves {n : Nat} (H : Group n) (p : Perm n) (h : ∀ (i : Fin H.generators.size), H.contains (p.conj H.generators[↑i]) = true) {q : Perm n} (hq : Generated H.generators q) : Generated H.generators (p.conj q)

theorem Hex.PermGroup.Search.Normalizer.test_iff {n : Nat} (H : Group n) (p : Perm n) : test H p = true ↔ ∀ (q : Perm n), Generated H.generators q ↔ Generated H.generators (p.conj q)

def Hex.PermGroup.Search.Predicate.normalizer {n : Nat} (H : Group n) : Predicate n

Equations

• Hex.PermGroup.Search.Predicate.normalizer H = { test := Hex.PermGroup.Search.Normalizer.test H, id := ⋯, comp := ⋯, inv := ⋯ }

theorem Hex.PermGroup.Search.Predicate.normalizer_iff {n : Nat} (H : Group n) (p : Perm n) : (normalizer H).test p = true ↔ ∀ (q : Perm n), Generated H.generators q ↔ Generated H.generators (p.conj q)