Solution (source code)

= Solution

Reducing coefficients modulo $p$ gives the <ring isomorphism>
$$
\mathbb Z[x]/(p,f)\cong\mathbb F_p[x]/(\bar f).
$$
If $d=\deg f>0$, its monic leading coefficient remains one modulo $p$, so $\deg\bar f=d$. <Polynomial division> gives a unique representative of degree less than $d$: existence follows by division, and the difference of two such representatives cannot be a nonzero multiple of a degree-$d$ monic <polynomial>. There are $p$ choices for each of the $d$ coefficients, proving
$$
\boxed{|\mathbb Z[x]/(p,f)|=p^d.}
$$
Irreducibility of $\bar f$ is not needed for finiteness; without it the <quotient ring> need not be a field.