Commit 2022-03-03 21:31 2c0fa829

feat(group_theory/free_product): the 🏓-lemma (#12210) The Ping-Pong-Lemma. If a group action of G on X so that the H i acts in a specific way on disjoint subsets X i we can prove that lift f is injective, and thus the image of lift f is isomorphic to the free product of the H i. Often the Ping-Pong-Lemma is stated with regard to subgroups H i that generate the whole group; we generalize to arbitrary group homomorphisms f i : H i →* G and do not require the group to be generated by the images. Usually the Ping-Pong-Lemma requires that one group H i has at least three elements. This condition is only needed if # ι = 2, and we accept 3 ≤ # ι as an alternative.