Commit 2021-07-13 20:14 63266ff4

View on Github →

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

Estimated changes

Modified docs/references.bib

Created src/group_theory/free_product.lean

added theorem free_product.ext_hom

added theorem free_product.induction_on

added theorem free_product.inv_def

added def free_product.lift

added theorem free_product.lift_of

added def free_product.of

added theorem free_product.of_apply

added theorem free_product.of_injective

added theorem free_product.of_left_inverse

added inductive free_product.rel

added def free_product