## 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: May 12 2021 at 07:17 UTC