mathlib

2f33463f - feat(group_theory/free_product): is_free_group_free_product_of_is_free_group (#12125)