theorem Hex.Graph.autos_complete {n : Nat} (G : Graph n) (h : 0 < n) {p : GraphIso.Perm n} (hp : G.IsIso G p) : GraphIso.Perm.Generated (G.autos h).gens p

Completeness: every graph automorphism is generated by the returned list.

theorem Hex.Graph.autos_sameOrbit {n : Nat} (G : Graph n) (h : 0 < n) (u v : Fin n) : (G.autos h).orbits[↑u]! = (G.autos h).orbits[↑v]! ↔ G.SameOrbit u v

Two vertices have the same representative exactly when they are in the same automorphism orbit.