Orbit-Stabiliser Theorem With Application to Rotational Symmetries

Jonas Rädle 📧

August 20, 2017

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


The Orbit-Stabiliser theorem is a basic result in the algebra of groups that factors the order of a group into the sizes of its orbits and stabilisers. We formalize the notion of a group action and the related concepts of orbits and stabilisers. This allows us to prove the orbit-stabiliser theorem. In the second part of this work, we formalize the tetrahedral group and use the orbit-stabiliser theorem to prove that there are twelve (orientation-preserving) rotations of the tetrahedron.
BSD License


Theories of Orbit_Stabiliser