def Hex.Perm.conj {n : Nat} (p q : Perm n) : Perm n

Conjugation in left-action order.

Equations

• p.conj q = p.comp (q.comp p.inv)

@[simp]

theorem Hex.Perm.conj_id {n : Nat} (p : Perm n) : p.conj (Perm.id n) = Perm.id n

@[simp]

theorem Hex.Perm.id_conj {n : Nat} (p : Perm n) : (Perm.id n).conj p = p

theorem Hex.Perm.conj_comp {n : Nat} (p q r : Perm n) : p.conj (q.comp r) = (p.conj q).comp (p.conj r)

theorem Hex.Perm.conj_inv {n : Nat} (p q : Perm n) : p.conj q.inv = (p.conj q).inv

theorem Hex.Perm.comp_conj {n : Nat} (p q r : Perm n) : (p.comp q).conj r = p.conj (q.conj r)

@[simp]

theorem Hex.Perm.inv_conj_conj {n : Nat} (p q : Perm n) : p.inv.conj (p.conj q) = q

@[simp]

theorem Hex.Perm.conj_inv_conj {n : Nat} (p q : Perm n) : p.conj (p.inv.conj q) = q

theorem Hex.PermGroup.Generated.conj {n : Nat} {S : Array (Perm n)} {q : Perm n} (hq : Generated S q) (p : Perm n) : Generated (Array.map p.conj S) (p.conj q)

def Hex.PermGroup.Group.conjugate {n : Nat} (p : Perm n) (G : Group n) : Group n

Conjugate every original generator and construct the resulting group.

Equations

• Hex.PermGroup.Group.conjugate p G = Hex.PermGroup.Group.ofGenerators (Array.map p.conj G.generators)

theorem Hex.PermGroup.Group.mem_conjugate {n : Nat} (p : Perm n) (G : Group n) (q : Perm n) : Generated (conjugate p G).generators q ↔ Generated G.generators (p.inv.conj q)