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{https://isa-afp.org/entries/Orbit_Stabiliser.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License