Solution (source code)

= Solution

The <product formula> says that every $x\in K^\times$ satisfies
$$
\prod_{v\in M_K}|x|_v^{d_v}=1.
$$
First suppose that $x$ is an <algebraic integer>. Its <principal ideal> has the <prime ideal factorization>
$$
(x)=\prod_{\mathfrak p}\mathfrak p^{\operatorname{ord}_{\mathfrak p}(x)}.
$$
Taking the <ideal norm> gives
$$
|N_{K/\mathbb Q}(x)|
=\prod_{\mathfrak p}p^{f_{\mathfrak p}\operatorname{ord}_{\mathfrak p}(x)}
=\prod_{v\text{ finite}}|x|_v^{-d_v}.
$$
On the other hand, the <field norm> is the product over embeddings, so
$$
|N_{K/\mathbb Q}(x)|
=\prod_{v\text{ infinite}}|x|_v^{d_v}.
$$
Equating these expressions proves the formula for algebraic integers. Every nonzero element of $K$ is a quotient of two algebraic integers, and multiplicativity completes the proof.