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

The commutator convention is [p,q] = p*q*p⁻¹*q⁻¹.

Equations

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

@[simp]

theorem Hex.Perm.comm_id {n : Nat} (p : Perm n) : p.comm (Perm.id n) = Perm.id n

@[simp]

theorem Hex.Perm.id_comm {n : Nat} (p : Perm n) : (Perm.id n).comm p = Perm.id n

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

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

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

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

theorem Hex.Perm.conj_comm {n : Nat} (g p q : Perm n) : g.conj (p.comm q) = (g.conj p).comm (g.conj q)

theorem Hex.Perm.comm_eq_id {n : Nat} (p q : Perm n) : p.comm q = Perm.id n ↔ p.comp q = q.comp p

theorem Hex.PermGroup.Normal.comm_generated {n : Nat} (G N : Group n) (hn : check G N = true) (hs : ∀ (p : Perm n), p ∈ G.generators → ∀ (q : Perm n), q ∈ G.generators → Generated N.generators (p.comm q)) (p q : Perm n) (hp : Generated G.generators p) (hq : Generated G.generators q) : Generated N.generators (p.comm q)

A normal subgroup containing original generator commutators contains all element commutators. The two inductions follow multiplication and inversion.