Commit 2025-10-23 13:34 d5b0059c
View on Github →feat(GroupTheory/FreeGroup/Orbit): The orbit of a point generated by parts of a free group can be "duplicated" (#30130)
Applying w⁻¹ to the orbit generated by all elements of a free group that start with w yields
the orbit generated by all the words that start with every letter execpt w⁻ (and the original point)
The orbit of a point x generated by a set of group elements s defined as all the points that can be reached by applying the elements of s to x.
A special case of this result is needed for the banach tarski theorem.