theorem Hex.GraphIso.Aut.orbitSize_card {n k : ℕ} (G : Colored n k) (v : Fin n) : orbitSize G v = Nat.card ↑(MulAction.orbit (↥(group G)) v)

The reported orbit length is the cardinality of the full group-action orbit.

noncomputable def Hex.GraphIso.Aut.orbitEquiv {n k : ℕ} (G : Colored n k) : MulAction.orbitRel.Quotient (↥(group G)) (Fin n) ≃ { v : Fin n // (orbits G)[↑v]! = ↑v }

Choosing the stored representative identifies the orbit quotient with precisely the vertices counted by numOrbits.

Equations

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

theorem Hex.GraphIso.Aut.numOrbits_card {n k : ℕ} (G : Colored n k) : numOrbits G = Nat.card (MulAction.orbitRel.Quotient (↥(group G)) (Fin n))

The reported orbit count is the cardinality of the full automorphism orbit quotient.