Existence of a Minkowski unit in a Galois number field

Let $K$ be a number field which is Galois over $\mathbb{Q}$, with Galois group $G = \mathrm{Gal}(K/\mathbb{Q})$ and ring of integers $\mathcal{O}_K$. Every $\sigma \in G$ restricts to a ring automorphism of $\mathcal{O}_K$ and hence acts on the unit group $\mathcal{O}_K^\times$.

Theorem (existence of a Minkowski unit). There is a unit $\varepsilon \in \mathcal{O}_K^\times$ such that the subgroup generated by its Galois conjugates

has finite index in $\mathcal{O}_K^\times$.

No hypothesis on the signature of $K$ is needed (it may be totally real, CM, or neither). Equivalently, $\mathbb{Q}\otimes_{\mathbb{Z}} \mathcal{O}_K^\times$ is a cyclic $\mathbb{Q}[G]$-module, generated by $1\otimes\varepsilon$; this is the classical starting point for the Galois-module approach to Leopoldt's conjecture (Ax, Brumer).

In the formal statement, $\sigma(\varepsilon)$ is Units.map (RingOfIntegers.mapRingEquiv σ.toRingEquiv) ε, the image of $\varepsilon$ under the restriction of $\sigma : K \simeq_{\mathbb{Q}} K$ to $\mathcal{O}_K$, and finite index is Subgroup.FiniteIndex.