feat(group_theory/free_product): the 🏓-lemma (#12210)
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.





leanprover-community/mathlib,leanprover-community/mathlib