mathlib3

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

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>