doc(group_theory/free_product): free not direct product (#17214)

Ping pong is for recognizing free products.  The conclusion of `lift_injective_of_ping_pong` should be documented as recognizing the image of `lift f` as the free product of the `H i`, not the direct product of the `H i`.



Co-authored-by: Jim Fowler <fowler@math.osu.edu>

src/group_theory/free_product.lean

@@ -676,7 +676,7 @@ The Ping-Pong-Lemma.
 
 Given 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
-direct product of the `H i`.
+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