Zulip Chat Archive

Stream: maths

Topic: group_hom

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.

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.)

Johan Commelin (Dec 12 2018 at 08:30):

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

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: Dec 20 2023 at 11:08 UTC