mathlib3

00980d9d - feat(group_theory/free_product): The ping pong lemma for free groups (#12916)

feat(group_theory/free_product): The ping pong lemma for free groups (#12916) We already have the ping-pong-lemma for free products; phrasing it for free groups is a (potentially) useful corollary, and brings us on-par with the Wikipedia page. Again, we state it as a lemma that gives a criteria for when `lift` is injective. Co-authored-by: Johan Commelin <johan@commelin.net>