def Hex.SparseGraph.autos {n : Nat} (G : SparseGraph n) : GraphIso.AutResult n

Native automorphism results for a bare sparse graph, using the zero-or-one-colour view and a single production traversal.

Equations

• G.autos = Hex.GraphIso.Sparse.autos G.toColored

theorem Hex.SparseGraph.autos_isIso {n : Nat} {G : SparseGraph n} {p : Perm n} (hp : p ∈ G.autos.gens) : G.IsIso G p

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

theorem Hex.SparseGraph.autos_sameOrbit {n : Nat} (G : SparseGraph n) (u v : Fin n) : G.autos.orbits[↑u]! = G.autos.orbits[↑v]! ↔ ∃ (p : Perm n), G.IsIso G p ∧ p.get u = v