division algorithm

Stream: Is there code for X?

[Faris Hafizhan Hakim]

Hi, I'm looking for the proof of the division algorithm in mathlib.

Let a and b be integers, with b > 0. Then there exist unique integers q and r such that a = bq + r where 0 <= r < b

I've tried searching in the nat, int, and number theory parts of mathlib but no luck. Any help appreciated. Thanks!

[Eric Wieser]

I think docs#int.div_add_mod is that statement

[Eric Wieser]

Where q = a / b and r = a % b

[Eric Wieser]

But I suppose that doesn't express uniqueness

[Faris Hafizhan Hakim]

I see, but it's not quite the same statement

[Faris Hafizhan Hakim]

I think the uniqueness is guaranteed by the uniqueness of % and /

[Kyle Miller]

docs#nat.div_mod_unique

[Kevin Buzzard]

Faris Hafizhan Hakim said:

I think the uniqueness is guaranteed by the uniqueness of % and /

This is not true. Just because they're well-defined functions giving answers which work, doesn't mean that there can't be other functions which also work. Kyle's answer is the right one.

[Faris Hafizhan Hakim]

Kevin Buzzard said:

This is not true. Just because they're well-defined functions giving answers which work, doesn't mean that there can't be other functions which also work. Kyle's answer is the right one.

Ah, okay, but then how does Kyle's answer express the uniqueness, that is, how is it different from Eric's answer? I don't quite understand. Thanks

[Faris Hafizhan Hakim]

Is it because of the m < k part?

[Kyle Miller]

docs#nat.div_add_mod and docs#nat.mod_lt give existence of the quotient and remainder (in the sense that they show that a / b is the quotient and a % b is the remainder), but then docs#nat.div_mod_unique gives uniqueness of the quotient and remainder (any other q and r with these properties must be a / b and a % b respectively), though admittedly since it's an iff it gives existence as well.

[Kyle Miller]

I didn't notice earlier that Eric gave the int rather than nat versions, and it seems that docs#int.div_mod_unique doesn't exist

[Kyle Miller]

Existence for int division is accounted for: there's docs#int.div_add_mod, docs#int.mod_nonneg, and docs#int.mod_lt_of_pos

[Kyle Miller]

Assuming it actually is missing, here's a sorry you or someone might fill and contribute to mathlib:

protected theorem int.div_mod_unique {a b r q : ℤ} (h : 0 < b) :
  a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < b :=
begin
  sorry
end

[Faris Hafizhan Hakim]

Hi, @Kyle Miller , I'm going to contribute to mathlib using the template you provided. How can I attribute you properly?

[Eric Wieser]

When you make the PR, it will give you a template that includes a "Co-authored-by" line; just fill that out with Kyle's name

[Nikolas Kuhn]

(deleted)