Group Amalgamation

Stream: Is there code for X?

[Hubert Ostoja-Petkowski]

Is group amalgamation (as in the construction used in the Seifert-Van Kampen Theorem) in mathlib? Free products are defined in group_theory.free_product, and family_of_elements.is_amalgamation is defined is category_theory.sites but this seems to be a different concept to group amalgamation.

[Adam Topaz]

You can use pushouts in docs#Group