What extra structure is needed so that grade-school arithmetic notions of division comes out of the formal definition of integer division?

Question

Formally, an integer $m$ divides an integer $n$ if $\exists k \in \mathbb{Z} | n = k\times m$. In grade school we took this further and say that the quotient $\frac{n}{m} = k$. However, this "equals" thing is not required in the formal definition.

One notable exception to the grade-school rule is that formally, $0|0$ because, $\forall k \in \mathbb{Z}, 0 = k\times0$. We wouldn't say that the quotient $\frac{0}{0} = $ any integer, because we expect the quotient to have a single value.

What additional mathematical structure is needed so that the grade-school idea of division is built up from the formal defitions?

Answer 1

I would say the most important thing here is the theorem that is usually referred to as the "divion algorithm":

Theorem: For any two integers $a$ and $b$ (with $b > 0$), there exist unique integers q and $r$, with $0 \leq r < b$, so that $$ a = q \cdot b + r $$

So the theorem tells us that we can always find $q$ and $r$, and in fact they are unique (we could not find a different $q$ and $r$ that also work). The "gradeschool" definition of $\frac{a}{b}$ is to define it to be the number $q$ guaranteed in this theorem in the case when $r$ ends up being zero.