Email Gateway (Aug 22 2022 at 15:55): Email Gateway (Aug 22 2022 at 15:55):From: Tobias Nipkow <nipkow@in.tum.de>
Orbit-Stabiliser Theorem with Application to Rotational Symmetries
Jonas Rädle
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.
https://www.isa-afp.org/entries/Orbit_Stabiliser.html
Enjoy!
smime.p7s
Last updated: Apr 19 2024 at 04:17 UTC