Brumer's theorem for $\mathbb{Q}(\zeta_n)$ with $\varphi(n) > 4$

Let $p$ be a prime and let $n$ be a natural number with $\varphi(n) > 4$, where $\varphi$ is Euler's totient function, so that $\mathbb{Q}(\zeta_n)$ is a totally complex field of degree $\varphi(n) \ge 6$ and unit rank $\varphi(n)/2 - 1 \ge 2$. Then the Leopoldt defect of the $n$-th cyclotomic field vanishes:

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

This is Brumer's theorem for cyclotomic fields in the range where it is not elementary. When $\varphi(n) \le 4$ the unit rank is at most $1$ and the vanishing follows from the general bound $\mathcal{D}_L(K) \le \operatorname{rank} \mathcal{O}_K^\times - 1$; for $\varphi(n) > 4$ one needs Brumer's $p$-adic analogue of Baker's theorem on linear forms in logarithms, applied to the cyclotomic units via the character decomposition of the $p$-adic regulator.

Formalization Note. CyclotomicField n ℚ is Mathlib's splitting field of the $n$-th cyclotomic polynomial over $\mathbb{Q}$. The hypothesis $4 < \varphi(n)$ excludes exactly the fields $\mathbb{Q}$ ($n = 0,1,2$), $\mathbb{Q}(\zeta_3)$, $\mathbb{Q}(i)$, $\mathbb{Q}(\zeta_5)$, $\mathbb{Q}(\zeta_8)$ and $\mathbb{Q}(\zeta_{12})$ (together with $n = 6, 10$, which give the same fields). No hypothesis relates $p$ to $n$.