Semilocal units become principal after a fixed power: $u^{M} \equiv 1 \pmod{\mathfrak{p}}$ for all $\mathfrak{p} \mid p$

Let $p$ be a prime and $\mathbb{F}$ a number field, with semilocal units $U_p(\mathbb{F}) = \prod_{\wp \mid p} \mathcal{O}_\wp^\times$ at $p$ (Section 1.1 of the source), where $\mathcal{O}_\wp$ is the ring of integers of the completion $\mathbb{F}_\wp$. Then there is an integer $M \ge 1$ such that for every $u \in U_p(\mathbb{F})$ and every prime $\wp \mid p$,

that is, $u^M$ lies in the product $\prod_{\wp \mid p} U_1(\mathbb{F}_\wp)$ of the principal units.

The point is that each residue field $\mathcal{O}_\wp / \wp\mathcal{O}_\wp \cong \mathcal{O}_\mathbb{F}/\wp$ is finite, say of order $q_\wp$, so the reduction of any local unit satisfies $\bar{u}^{\,q_\wp - 1} = 1$ and $u^{q_\wp - 1} \equiv 1 \pmod{\wp}$; the product $M = \prod_{\wp \mid p} (q_\wp - 1)$ then works for all coordinates at once. Equivalently, the principal units form a subgroup of finite index in the local units, and $M$ is a multiple of the exponent of the finite quotient $\prod_{\wp \mid p} (\mathcal{O}_\wp/\wp)^\times$.

This is the step that moves a rank question from the full semilocal units, where the platform's definitions live, to the principal units, which carry the $\mathbb{Z}_p$-module structure of Definitions.Def_OneUnits: raising a continuous injection $\mathbb{Z}_p^{\,n} \hookrightarrow U_p(\mathbb{F})$ to the $M$-th power keeps it injective and continuous and lands it in $\prod_{\wp \mid p} U_1(\mathbb{F}_\wp)$, where Leopoldt.natCast_le_rank_of_continuous_injective applies.

Formalization Note The coordinate $u_\wp$ is a unit of v.1.adicCompletionIntegers F and is coerced into the completion v.1.adicCompletion F to take the norm, exactly as in the hypothesis of Leopoldt.natCast_le_rank_of_continuous_injective. Finiteness of the residue field of the completion is not available in Mathlib at this revision as a ready-made instance; it has to be obtained from the finiteness of $\mathcal{O}_\mathbb{F}/\wp$ and the identification of residue fields, or from a direct argument with the norm.