Solution (source code)

= Solution

For a <number field> with $r$ real embeddings $\sigma_i$ and $s$ conjugate pairs of complex embeddings $\tau_j$, use the <logarithmic embedding of number field units>
$$
\ell(u)=(\log|\sigma_1u|,\ldots,\log|\sigma_ru|,2\log|\tau_1u|,\ldots,2\log|\tau_su|).
$$
It is a <group homomorphism> from multiplication to addition. A <unit> has <field norm> $\pm1$, so the coordinates sum to zero. Deleting one coordinate identifies this hyperplane with $\mathbb R^{r+s-1}$ and gives the desired map.

If its image coordinates remain in a bounded set, the omitted coordinate is bounded too, and every conjugate of $u$ has bounded absolute value. The coefficients of its monic <minimal polynomial> are <integers> and elementary symmetric expressions in at most $[K:\mathbb Q]$ bounded conjugates. They are therefore bounded <integers>. Only finitely many such <polynomials>, and finitely many roots of them, exist. Thus the inverse image of every bounded set is finite. In particular \b[the kernel is finite and the image is discrete]. This argument includes the zero-dimensional target case; it does not yet assert the full-rank part of <Dirichlet unit theorem>.