rotation of cube

Stream: mathlib4

[BANGJI HU]

image.png
i try to use burnside lemma to formal the color problem,which is complicate,but first how to present the rotation of cube,and i consider the cube as s8 my point is how to make sure the permutation is the subgroup for example
how to use lean to make that per（1234）（5678）is the rotation of cube

[Aaron Liu]

You could define an action of S4 on the vertices of the cube, and then your subgroup is just the orbit of the identity.

[BANGJI HU]

What is an equivalent proposition to coloring the 6 faces of a cube with 6 different colors?

[Edward van de Meent]

define a map from the type of faces to the type of colors?