mathlib

63266ff4 - feat(group_theory/free_product): the free product of an indexed family of monoids (#8256)

feat(group_theory/free_product): the free product of an indexed family of monoids (#8256) Defines the free product (categorical coproduct) of an indexed family of monoids. Proves its universal property. The free product of groups is a group. Split off from #7395