Homomorphism $\mathbb{Z}[\theta]\to\mathbb{Z}/n\mathbb{Z}$, $\theta\mapsto m$

Let $f \in \mathbb{Z}[x]$ be irreducible in $\mathbb{Z}[x]$, let $\theta \in \mathbb{C}$ be a root of $f$, let $n \in \mathbb{N}$ and $m \in \mathbb{Z}$ with

Then there is a ring homomorphism $\varphi : \mathbb{Z}[\theta] \to \mathbb{Z}/n\mathbb{Z}$ with $\varphi(\theta) = m \bmod n$, where $\mathbb{Z}[\theta]$ is the subring of $\mathbb{C}$ generated by $\theta$.

This homomorphism turns square roots computed in the number field into residues modulo $n$.

Formalization Note Irreducibility in $\mathbb{Z}[x]$ (rather than only over $\mathbb{Q}$) includes primitivity, which is necessary: for $f(x)=2x$ and $n=2$ the conclusion fails for $m=1$. For $n = 0$, $\mathbb{Z}/0\mathbb{Z}$ is $\mathbb{Z}$.