by basic properties of groups,
and by ^P5.
Note that this homomorphism is completely determined from the fact , hence it is unique.
By standard Euclidean division, forms a Euclidean domain.
In some number-theoretic contexts, these are referred to as the rational integers to distinguish them from algebraic integers.