has_div

Stream: general

[Johan Commelin]

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]

Is this right division or left division?

[Mario Carneiro]

Why?

[Mario Carneiro]

I don't think uniformity is a good reason

[Mario Carneiro]

I would expect that it is right division

[Mario Carneiro]

the usual notation for left division is \

[Mario Carneiro]

plus the additive version uses right subtraction

[Johan Commelin]

Why is uniformity not a good reason?

[Mario Carneiro]

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]

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]

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

[Johan Commelin]

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]

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]

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

[Chris Hughes]

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