has_div for groups

Stream: maths

[Johan Commelin]

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

[Kenny Lau]

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

[Kenny Lau]

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)