Orbit-Stabiliser Theorem with Application to Rotational Symmetries

Title:	Orbit-Stabiliser Theorem with Application to Rotational Symmetries
Author:	Jonas Rädle (jonas /dot/ raedle /at/ tum /dot/ de)
Submission date:	2017-08-20
Abstract:	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.
BibTeX:	@article{Orbit_Stabiliser-AFP, author = {Jonas Rädle}, title = {Orbit-Stabiliser Theorem with Application to Rotational Symmetries}, journal = {Archive of Formal Proofs}, month = aug, year = 2017, note = {\url{http://isa-afp.org/entries/Orbit_Stabiliser.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.