@[instance_reducible]

instance Hex.GraphIso.instGroupPerm_hexGraphIsoMathlib {n : ℕ} : Group (Perm n)

Equations

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

@[simp]

theorem Hex.GraphIso.Perm.mul_get {n : ℕ} (p q : Perm n) (v : Fin n) : (p * q).get v = p.get (q.get v)

@[simp]

theorem Hex.GraphIso.Perm.one_get {n : ℕ} (v : Fin n) : get 1 v = v

@[instance_reducible]

noncomputable instance Hex.GraphIso.instFintypePerm_hexGraphIsoMathlib {n : ℕ} : Fintype (Perm n)

Equations

• Hex.GraphIso.instFintypePerm_hexGraphIsoMathlib = Fintype.ofInjective Hex.GraphIso.Perm.toEquiv ⋯

@[instance_reducible]

instance Hex.GraphIso.instMulActionPermFin_hexGraphIsoMathlib {n : ℕ} : MulAction (Perm n) (Fin n)

Equations

• Hex.GraphIso.instMulActionPermFin_hexGraphIsoMathlib = { smul := Hex.GraphIso.Perm.get, mul_smul := ⋯, one_smul := ⋯ }

def Hex.GraphIso.Aut.group {n k : ℕ} (G : Colored n k) : Subgroup (Perm n)

The full colour-preserving automorphism group, as a subgroup of the executable permutations.

Equations

• Hex.GraphIso.Aut.group G = { carrier := {p : Hex.GraphIso.Perm n | Hex.GraphIso.IsIso G G p}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem Hex.GraphIso.Aut.mem_group {n k : ℕ} (G : Colored n k) (p : Perm n) : p ∈ group G ↔ IsIso G G p

theorem Hex.GraphIso.Aut.closure_eq_group {n k : ℕ} (G : Colored n k) : Subgroup.closure {p : Perm n | p ∈ gens G} = group G

The subgroup generated by the returned list is the full automorphism group.

theorem Hex.GraphIso.Aut.mem_orbit {n k : ℕ} (G : Colored n k) (u v : Fin n) : v ∈ MulAction.orbit (↥(group G)) u ↔ SameOrbit G u v

The group-action orbit relation is the executable graph's automorphism orbit relation.