[isabelle] New AFP entry: Orbit-Stabiliser Theorem with Application to Rotational Symmetries



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!

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.