The $\mathbb{Z}_p$-rank of the principal units of $F_v$ is at most $e_v f_v$

Let $p$ be a prime, $F$ a number field and $v$ a prime of $\mathcal{O}_F$ above $p$, with completion $F_v$. Write $e_v$ and $f_v$ for the ramification index and the inertia degree of $v$ over $p$, so that $e_v f_v = [F_v : \mathbb{Q}_p]$. The principal units $U^{1}(F_v) = \{u \in F_v^\times : \|u - 1\| < 1\}$ form a $\mathbb{Z}_p$-module under $p$-adic exponentiation (OneUnits.instModule of Definitions.Def_OneUnits). The statement asserts

where the rank is Mathlib's Module.rank, the supremum of the cardinalities of $\mathbb{Z}_p$-linearly independent families.

This is the local input of the bound $\operatorname{rank}_{\mathbb{Z}_p} \prod_{v \mid p} U^{1}(F_v) \le [F : \mathbb{Q}]$ (Leopoldt.rank_oneUnits_le_finrank), which follows from it by the fundamental identity $\sum_{v \mid p} e_v f_v = [F : \mathbb{Q}]$. The expected proof is the classical one: the $p$-adic logarithm maps $U^{1}(F_v)$ $\mathbb{Z}_p$-linearly into $F_v$ with torsion kernel, and $F_v$ has $\mathbb{Z}_p$-rank $[F_v : \mathbb{Q}_p] = e_v f_v$. Neither the $p$-adic logarithm nor the $\mathbb{Q}_p$-algebra structure on $F_v$ is in Mathlib yet, so both would have to be built; an alternative avoiding the logarithm is the filtration by higher unit groups, whose graded pieces are finite of order $|\mathcal{O}_F / v| = p^{f_v}$ and on which the $p$-th power map acts as a shift by $e_v$.