The local degree formula: $\operatorname{rk}_{\mathbb{Z}_p} \mathbb{F}_\wp \le ef$

Let $p$ be a prime, $\mathbb{F}$ a number field and $\wp$ a prime of $\mathcal{O}(\mathbb{F})$ above $p$, and let $\mathbb{F}_\wp$ be the completion. Write $e = e(\wp \mid p)$ for the ramification index and $f = f(\wp \mid p)$ for the residue degree of $\wp$ over $\mathbb{Z}$. Then, as a $\mathbb{Z}_p$-module,

This is the local degree formula $[\mathbb{F}_\wp : \mathbb{Q}_p] = ef$, in the form of an inequality of $\mathbb{Z}_p$-ranks. Its global counterpart, $\sum_{\wp \mid p} e_\wp f_\wp = [\mathbb{F}:\mathbb{Q}]$, is in Mathlib; the local statement — that completing at $\wp$ turns that summand into the degree of the completion over $\mathbb{Q}_p$ — is not.

The classical proof is that $\mathcal{O}_\wp$ is a free $\mathbb{Z}_p$-module with basis $\{\pi^i \omega_j\}_{0 \le i < e,\ 0 \le j < f}$, where $\pi$ is a uniformiser and the $\omega_j$ lift a basis of the residue field over $\mathbb{F}_p$; the field $\mathbb{F}_\wp$ is $\mathcal{O}_\wp[1/p]$, of the same rank. Only the upper bound is asserted here, which is all that the applications need.

Formalization note. The $\mathbb{Z}_p$-algebra structure on $\mathbb{F}_\wp$ is the one supplied by Definitions.Def_PadicLog: the canonical map $\mathbb{Z}_p \to \mathbb{F}_\wp$ obtained as the limit of the integer approximations. Ideal.ramificationIdx and Ideal.inertiaDeg are taken relative to $\mathbb{Z}$, matching the shape in which the mission's statement Leopoldt.rank_oneUnits_le_ramificationIdx_mul_inertiaDeg uses them.