Zulip Chat Archive

Stream: Is there code for X?

Topic: monoid_hom.map_div

Eric Wieser (Jul 29 2021 at 16:20):

Was it a conscious decision to have docs#add_monoid_hom.map_sub but not docs#monoid_hom.map_div?

Eric Wieser (Jul 29 2021 at 16:21):

I was expected the former to just be generated as an additive version of the latter

Anne Baanen (Jul 29 2021 at 16:50):

Probably not, group didn't have a division operator until a couple of months ago, so there are many places where the non-additive versions of sub are missing.

Eric Wieser (Jul 29 2021 at 20:30):

I added those lemmas into #8461

Last updated: Dec 20 2023 at 11:08 UTC