The different of a number field

The different of $K$ is ${\mathfrak{D}}_K=({\mathcal{O}}_K^{\vee }{)}^{-1}=\{x\in K:x{\mathcal{O}}_K^{\vee }\subseteq {\mathcal{O}}_K\}\mathrm{.}$ Here $K$ is a number field and ${\mathcal{O}}_K^{\vee }$ is its nonzero fractional codifferent (The codifferent is a fractional ideal). To justify the inverse using Integral ideal factorisation in a number field, in ZF, let $\mathfrak{p}$ be a nonzero prime and choose $0\mathrm{\ne }a\in \mathfrak{p}$. Factor $(a)$ into finitely many nonzero prime ideals. Since their product lies in $\mathfrak{p}$, one factor lies in $\mathfrak{p}$ and equals it: nonzero primes of ${\mathcal{O}}_K$ are maximal, as their quotients are finite domains. Thus $(a)=\mathfrak{p}\mathfrak{b}$ for an integral ideal $\mathfrak{b}$, and $\mathfrak{p}(a^{-1}\mathfrak{b})={\mathcal{O}}_K$. Factoring an arbitrary nonzero integral ideal now gives an inverse by taking the finite product of these prime inverses; clearing a denominator gives an inverse for every nonzero fractional ideal. All choices are finite. By Invertible fractional ideals this inverse is the displayed colon ideal. Also ${\mathcal{O}}_K\subseteq {\mathcal{O}}_K^{\vee }$, since traces of algebraic integers are integers. Multiplying this inclusion by $({\mathcal{O}}_K^{\vee }{)}^{-1}$ gives ${\mathfrak{D}}_K\subseteq {\mathcal{O}}_K$, so the different is an integral ideal.