Zulip Chat Archive

Stream: maths

Topic: group_hom


view this post on Zulip Chris Hughes (Dec 12 2018 at 06:17):

Can we define is_group_hom to be is_monoid_hom and make it reducible? It would avoid cycles.

view this post on Zulip Johan Commelin (Dec 12 2018 at 08:30):

I would like this too. Especially if we could fill in the condition f 1 = 1 using some default argument or auto_param. (Because for groups, as opposed to monoid, you can derive this condition from the multiplicativity.)

view this post on Zulip Johan Commelin (Dec 12 2018 at 08:30):

Whether it should be reducible, I don't know.

view this post on Zulip Chris Hughes (Dec 12 2018 at 08:40):

If it's reducible then every group hom is automatically a monoid hom and vice versa


Last updated: May 12 2021 at 07:17 UTC