Zulip Chat Archive

Stream: maths

Topic: uniqueness of division and remainder


view this post on Zulip Kevin Buzzard (Nov 04 2019 at 13:22):

Do we have anything like this

example (a q b r : ℤ) (hb : b > 0) : a = r + b * q → 0 ≤ r → r < b → r = a % b := sorry

in mathlib already? One could also prove q = a / b. I can prove them, I just don't want to.

Related: if b > 0 is an integer and 0 <= r < b is a multiple of b then r = 0. Do we have this?

view this post on Zulip Chris Hughes (Nov 04 2019 at 13:23):

I remember something called div_mod_unique. It might only be for nat.

view this post on Zulip Kevin Buzzard (Nov 04 2019 at 13:23):

Well remembered and yes it's only for nat, so it seems. Thanks.

view this post on Zulip Kevin Buzzard (Nov 04 2019 at 13:26):

protected theorem div_mod_unique {n k m d : } (h : 0 < k) :
  n / k = d  n % k = m  m + k * d = n  m < k :=

What are the chances that the user has those facts in exactly that way so they can rewrite? Both sides have an \and :-/ The int version will have the additional hypothesis that m>=0 as well :-/

view this post on Zulip Mario Carneiro (Nov 04 2019 at 13:38):

it's not for rewriting like that, but you can always rewrite with ((div_mod_unique h1).2 <h2, h3>).2

view this post on Zulip Kevin Buzzard (Nov 04 2019 at 15:49):

Fair point.


Last updated: May 11 2021 at 16:22 UTC