$\operatorname{rank}_{\mathbb{Z}_p} \prod_{\mathfrak{p} \mid p} U_1(\mathbb{F}_\mathfrak{p}) \le [\mathbb{F} : \mathbb{Q}]$

Let $p$ be a prime and $\mathbb{F}$ a number field. For each prime $\wp \mid p$ let $U_1(\mathbb{F}_\wp) = \{u \in \mathbb{F}_\wp^\times : \|u - 1\| < 1\}$ be the principal units of the completion, a topological $\mathbb{Z}_p$-module by Definitions.Def_OneUnits and Definitions.Def_PrimesOverNorm. Then

This is the structure theory of local units: for each $\wp \mid p$ the group $U_1(\mathbb{F}_\wp)$ is the direct product of its finite torsion subgroup (the $p$-power roots of unity in $\mathbb{F}_\wp$) and a free $\mathbb{Z}_p$-module of rank $[\mathbb{F}_\wp : \mathbb{Q}_p]$, for instance because the $p$-adic logarithm maps a subgroup of finite index isomorphically onto a lattice in $\mathbb{F}_\wp$; and the local degrees add up to the global one, $\sum_{\wp \mid p} [\mathbb{F}_\wp : \mathbb{Q}_p] = [\mathbb{F} : \mathbb{Q}]$, because $\mathbb{F} \otimes_\mathbb{Q} \mathbb{Q}_p \cong \prod_{\wp \mid p} \mathbb{F}_\wp$. Only the resulting inequality is asserted here.

It is the fact behind the bound argument of the mission's definition of the Leopoldt defect: the $\mathbb{Z}_p$-rank of the $p$-adic closure $\bar{E}(\mathbb{F})$ of the global units, a subgroup of the semilocal units, never exceeds $[\mathbb{F} : \mathbb{Q}]$, which is why zpRankBelow p (finrank ℚ F) measures the true rank. Together with Leopoldt.exists_pow_mem_oneUnits and the bridge Leopoldt.natCast_le_rank_of_continuous_injective it yields Leopoldt.le_finrank_of_continuous_injective_semilocalUnits, the bound needed on the frontier of Remark 1.A.

Formalization Note The rank is Mathlib's Module.rank ℤ_[p], a cardinal, of the product module ∀ v : PrimesOver p F, Additive (oneUnits (v.1.adicCompletion F)), compared with the natural number Module.finrank ℚ F cast to a cardinal. No $\mathbb{Q}_p$-algebra structure on the completions is assumed in the statement; a proof through local degrees will have to construct the map $\mathbb{Q}_p \to \mathbb{F}_\wp$ or argue through the filtration of the principal units by the $p$-power maps instead.