The units of a finite extension are generated, up to finite index, by the units of the base field and $\mathrm{rk}\,E(\mathbb{K}) - \mathrm{rk}\,E(\mathbb{F})$ further units

Let $\mathbb{K}/\mathbb{F}$ be a finite extension of number fields and write $E(\mathbb{F}) = \mathcal{O}(\mathbb{F})^\times$ and $E(\mathbb{K}) = \mathcal{O}(\mathbb{K})^\times$ for their unit groups, with Dirichlet ranks $\mathrm{rk}\,E(\mathbb{F}) = r_1(\mathbb{F}) + r_2(\mathbb{F}) - 1$ and $\mathrm{rk}\,E(\mathbb{K}) = r_1(\mathbb{K}) + r_2(\mathbb{K}) - 1$. The inclusion $\mathcal{O}(\mathbb{F}) \subseteq \mathcal{O}(\mathbb{K})$ embeds $E(\mathbb{F})$ into $E(\mathbb{K})$.

Then there exist an integer $m \ge 0$ and units $g_1, \dots, g_m \in E(\mathbb{K})$ such that

In words: the $\mathbb{Z}$-generators of the units of $\mathbb{K}$ are those of $\mathbb{F}$ together with at most $\mathrm{rk}\,E(\mathbb{K}) - \mathrm{rk}\,E(\mathbb{F})$ further units, up to a subgroup of finite index. This is the algebraic half of Remark 1.A of the source, which compares the "linear relations between $\mathbb{Z}$-generators of the units" of a field and of a finite extension: it bounds how many new generators the extension can contribute, so that any growth of the $p$-adic rank of the closure of the units along $\mathbb{K}/\mathbb{F}$ is charged to at most $\mathrm{rk}\,E(\mathbb{K}) - \mathrm{rk}\,E(\mathbb{F})$ elements. Together with the corresponding bound on the $\mathbb{Z}_p$-rank of the $p$-adic closure (Leopoldt.zpRankBelow_unitClosure_le_add_of_finiteIndex) it yields that a positive Leopoldt defect is inherited by finite extensions.

Formalization Note The fields are related by an Algebra F K instance with FiniteDimensional F K, exactly as in the milestone statement Leopoldt.defect_pos_of_defect_pos; the embedding of unit groups is Units.map of the ring map $\mathcal{O}(\mathbb{F}) \to \mathcal{O}(\mathbb{K})$, and the subgroup generated by $E(\mathbb{F})$ and the $g_i$ is the join of the range of that map with the subgroup closure of $\{g_1,\dots,g_m\}$. Dirichlet's rank is Mathlib's NumberField.Units.rank. The number $m$ is existentially quantified with $m + \mathrm{rk}\,E(\mathbb{F}) \le \mathrm{rk}\,E(\mathbb{K})$ rather than fixed as a truncated difference, so the statement carries the inequality $\mathrm{rk}\,E(\mathbb{F}) \le \mathrm{rk}\,E(\mathbb{K})$ with it.