Zulip Chat Archive

Stream: mathlib4

Topic: Monoid coproduct

Yury G. Kudryashov (Sep 07 2023 at 20:39):

Hi,
I noticed that binary coproducts of monoids/groups were recently merged in #6828. I have a more extensive theory in #2214 and was waiting for a dependency (#6913) to rename it & fix CI. @Chris Hughes @Johan Commelin What should we do?

Chris Hughes (Sep 07 2023 at 21:19):

I didn't use anything except the universal property, so as long as we keep that I'm fine with any refactors. I also don't have plans to add to the theory.

Johan Commelin (Sep 08 2023 at 04:15):

@Yury G. Kudryashov Aha, I wasn't aware of this. Sorry.
I haven't yet reviewed your PR. Is there a lot of overlap with #6828?

Yury G. Kudryashov (Sep 08 2023 at 05:42):

I'll merge master and merge APIs. I think that my API is a superset of Chris's but it's possible that there it misses a few lemmas.

Yury G. Kudryashov (Sep 14 2023 at 06:55):

I merged master and tried to add missing bits of API to my file. @Chris Hughes , could you please have a look?

Yury G. Kudryashov (Sep 14 2023 at 06:55):

#2214

Chris Hughes (Sep 14 2023 at 13:31):

master will have to be merged again because !4#6923 just got merged.

Yury G. Kudryashov (Sep 14 2023 at 13:57):

BTW, could you please add names Graham Higman, Bernhard Neumann, and Hanna Neumann to the module docstring of the file about HNN extension?

Yury G. Kudryashov (Sep 14 2023 at 18:03):

Merged, fixed compile.

Last updated: Dec 20 2023 at 11:08 UTC