The $\mathbb{Z}_p$-rank of the $p$-adic closure of the units grows by at most the number of new unit generators

Let $p$ be a prime and let $\mathbb{K}/\mathbb{F}$ be a finite extension of number fields. For a number field $\mathbb{L}$ write $E(\mathbb{L}) = \mathcal{O}(\mathbb{L})^\times$ for its units, $U_p(\mathbb{L}) = \prod_{\wp \mid p} \mathcal{O}_\wp^\times$ for the semilocal units at $p$, $\iota : E(\mathbb{L}) \to U_p(\mathbb{L})$ for the diagonal embedding, and

for the $p$-adic closure of the global units, as in Section 1.1 of the source. Suppose that $g_1, \dots, g_m \in E(\mathbb{K})$ are units such that the subgroup $E(\mathbb{F}) \cdot \langle g_1, \dots, g_m \rangle$ generated by the units of $\mathbb{F}$ and the $g_i$ has finite index in $E(\mathbb{K})$. Then

This is the topological half of Remark 1.A of the source: the linear relations among the units of $\mathbb{F}$ that arise upon $p$-adic completion are preserved under the embedding $E(\mathbb{F}) \hookrightarrow E(\mathbb{K})$, so passing to $\mathbb{K}$ can raise the $\mathbb{Z}_p$-rank of the closure only through the $m$ new generators. The semilocal units of $\mathbb{F}$ embed continuously and injectively into those of $\mathbb{K}$ compatibly with the diagonal embeddings (the construction behind Leopoldt.zpRankBelow_unitClosure_mono), and a subgroup of finite index has the same $\mathbb{Z}_p$-rank of closure, so the closure of $E(\mathbb{K})$ is, up to a finite group, topologically generated by the image of $\bar{E}(\mathbb{F})$ and the $m$ elements $\iota(g_i)$. Combined with the algebraic bound $m \le \mathrm{rk}\,E(\mathbb{K}) - \mathrm{rk}\,E(\mathbb{F})$ on the number of new generators (Leopoldt.exists_finiteIndex_units_sup_closure), it gives $\mathcal{D}_L(\mathbb{F}) \le \mathcal{D}_L(\mathbb{K})$, and in particular that a positive Leopoldt defect is inherited by finite extensions.

Formalization Note The two fields are related by an Algebra F K instance with FiniteDimensional F K, as in the milestone statement Leopoldt.defect_pos_of_defect_pos. The subgroup $E(\mathbb{F})\cdot\langle g_1,\dots,g_m\rangle$ is the join of the range of Units.map of the ring map $\mathcal{O}(\mathbb{F}) \to \mathcal{O}(\mathbb{K})$ with the subgroup closure of $\{g_1, \dots, g_m\}$, and finite index is Mathlib's Subgroup.FiniteIndex. The $\mathbb{Z}_p$-ranks are zpRankBelow p (finrank ℚ ·) (unitClosure p ·) of the definition file, each with its own field's degree over $\mathbb{Q}$ as the bound argument, exactly as they enter the definition of the defect; since the $\mathbb{Z}_p$-rank of $\bar{E}(\mathbb{L})$ never exceeds that of $U_p(\mathbb{L})$, which is $[\mathbb{L} : \mathbb{Q}]$, the bounds never constrain the ranks.