Zulip Chat Archive

Stream: general

Topic: has_div


view this post on Zulip Johan Commelin (May 27 2020 at 09:49):

Should we, in the name of uniformity, add a has_div instance for group to match the has_sub for add_group? And then fix all the lemmas that existing for has_sub to have a multiplicative counterpart.

view this post on Zulip Gabriel Ebner (May 27 2020 at 09:53):

Is this right division or left division?

view this post on Zulip Mario Carneiro (May 27 2020 at 09:56):

Why?

view this post on Zulip Mario Carneiro (May 27 2020 at 09:56):

I don't think uniformity is a good reason

view this post on Zulip Mario Carneiro (May 27 2020 at 09:57):

I would expect that it is right division

view this post on Zulip Mario Carneiro (May 27 2020 at 09:58):

the usual notation for left division is \

view this post on Zulip Mario Carneiro (May 27 2020 at 09:59):

plus the additive version uses right subtraction

view this post on Zulip Johan Commelin (May 27 2020 at 10:02):

Why is uniformity not a good reason?

view this post on Zulip Mario Carneiro (May 27 2020 at 10:08):

Every definition comes with an obligation to a whole load of theorems because of the aforementioned pairwise interaction of concepts. So I think we should try to stick to things that are directly useful, either because they are used in maths or because they are useful to unify formal proof developments

view this post on Zulip Chris Hughes (May 27 2020 at 11:23):

Is there a reason why division isn't just notation for multiplication by the inverse? If we changed the notation for int division this could be done.

view this post on Zulip Reid Barton (May 27 2020 at 11:42):

Well this won't work for nat division--whether this is a good thing is a separate question

view this post on Zulip Johan Commelin (May 27 2020 at 11:44):

We could still add has_div if has_mul and has_inv are present. That wouldn't give instance conflicts for nat and int.

view this post on Zulip Chris Hughes (May 27 2020 at 12:05):

We already have that. The point of making it notation is that we don't have to prove a bunch of lemmas, and the pretty printer looks nicer as well.

view this post on Zulip Johan Commelin (May 27 2020 at 12:07):

@Chris Hughes Do we? I thought we couldn't use div in random groups

view this post on Zulip Chris Hughes (May 27 2020 at 12:08):

Oh, we probably don't actually. Just for division rings.


Last updated: May 16 2021 at 21:11 UTC