Brumer's theorem for $\mathbb{Q}(\zeta_m)$ with $4p \mid m$

Let $p$ be a prime and let $m \ge 1$ be a natural number divisible by $4p$, so that the $m$-th cyclotomic field $\mathbb{K} = \mathbb{Q}(\zeta_m)$ contains the $p$-th roots of unity $\mu_p$ and the fourth roots of unity $\mu_4$ (for $p = 2$: the eighth roots of unity). Then the Leopoldt defect of $\mathbb{K}$ at $p$ vanishes:

Here $\mathcal{D}_L(\mathbb{K}) = \operatorname{rank}_{\mathbb{Z}} E(\mathbb{K}) - \operatorname{rank}_{\mathbb{Z}_p} \overline{E}(\mathbb{K})$ is the defect of Section 1.1 of the mission source, $E(\mathbb{K}) = \mathcal{O}_{\mathbb{K}}^\times$ being the global units and $\overline{E}(\mathbb{K})$ the closure of their diagonal image in the product $\prod_{\wp \mid p} \mathcal{O}_\wp^\times$ of the local unit groups at the primes above $p$.

This is Brumer's theorem (Leopoldt's conjecture for abelian number fields) for the cofinal family of cyclotomic fields whose level is divisible by $4p$. Such a field is Galois over $\mathbb{Q}$, CM, and contains the $p$-th roots of unity, as the working base field of the mission source does; the additional requirement $4 \mid m$ is a convenience normalisation not taken from the source. By Remark 1.A of the source (a positive defect is inherited by finite extensions), Leopoldt's conjecture for $\mathbb{Q}(\zeta_m)$ implies it for every subfield, in particular for every $\mathbb{Q}(\zeta_n)$ with $n \mid m$; since every $n \ge 1$ divides $4pn$, this family determines the conjecture for all cyclotomic fields.

Formalization Note. CyclotomicField m ℚ is Mathlib's splitting field of the $m$-th cyclotomic polynomial over $\mathbb{Q}$. The hypothesis $0 < m$ excludes the degenerate level $m = 0$ (divisible by every integer, with CyclotomicField 0 ℚ equal to $\mathbb{Q}$); the statement would remain true there, but the exclusion keeps the family equal to the cyclotomic fields containing $\mu_{4p}$.