## Stream: general

### Topic: has_div

#### 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.

#### Gabriel Ebner (May 27 2020 at 09:53):

Is this right division or left division?

Why?

#### Mario Carneiro (May 27 2020 at 09:56):

I don't think uniformity is a good reason

#### Mario Carneiro (May 27 2020 at 09:57):

I would expect that it is right division

#### Mario Carneiro (May 27 2020 at 09:58):

the usual notation for left division is \

#### Mario Carneiro (May 27 2020 at 09:59):

plus the additive version uses right subtraction

#### Johan Commelin (May 27 2020 at 10:02):

Why is uniformity not a good reason?

#### 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

#### 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.

#### 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

#### 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.

#### 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.

#### Johan Commelin (May 27 2020 at 12:07):

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

#### 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