Zulip Chat Archive

Stream: maths

Topic: has_div for groups


view this post on Zulip Johan Commelin (Apr 09 2019 at 01:01):

Is there a particular reason why we have has_sub for add_groups, but not has_div for groups?

view this post on Zulip Kenny Lau (Apr 09 2019 at 01:34):

because you don't write a/b for a, b \in G

view this post on Zulip Kenny Lau (Apr 09 2019 at 01:36):

you might wonder why division isn't defined for groups, and this is one of the differences from add_groups, which have subtraction, but there is a difference between the total division on groups and the almost total division on fields and it doesn't seem to be helpful to unify them; lots of theorems overlap with a name conflict, but they are all proven differently

:point_up: Mario Carneiro, 15/01/2019 12:24:17 (UTC)


Last updated: May 18 2021 at 07:19 UTC