ThmDex – An index of mathematical definitions, results, and conjectures.
Result R560 on D569: Integer divisor
Division theorem in the ring of basic integers
Formulation 1
Let $R = (\mathbb{Z}, +, \cdot)$ be the D588: Ring of integers.
Let $a, b \in \mathbb{Z}$ each be a D5094: Positive integer such that
(i) \begin{equation} a \neq 0 \end{equation}
Then \begin{equation} \# \{ (q, r) \in \mathbb{Z} \times \mathbb{Z} : b = a q + r \text{ and } 0 \leq r < |a| \} = 1 \end{equation}
Formulation 2
Let $R = (\mathbb{Z}, +, \cdot)$ be the D588: Ring of integers.
Let $a, b \in \mathbb{Z}$ each be a D5094: Positive integer such that
(i) \begin{equation} a \neq 0 \end{equation}
Then \begin{equation} \exists \, ! \, (q, r) \in \mathbb{Z} \times \mathbb{Z} : b = a q + r \text{ and } 0 \leq r < |a| \end{equation}