Commit 2023-12-15 09:19 e216be2a
View on Github →feat: noncommutative coproduct for MonoidHom (#7335)
Add MonoidHom.noncommCoprod which allows to define a morphism from a product M x N
to a monoid P given two monoid morphisms M -> P and N -> P,
provided a commutativity assumption on the ranges.