Leopoldt's conjecture for totally real multiquadratic fields

Leopoldt's conjecture holds, at every prime $p$, for every totally real multiquadratic field. Precisely: let $\mathbb{K}$ be a totally real number field, Galois over $\mathbb{Q}$, such that every element of $G = \mathrm{Gal}(\mathbb{K}/\mathbb{Q})$ satisfies $\sigma^2 = 1$. Then

Here $E = \mathcal{O}_{\mathbb{K}}^\times$ and $\overline{E}$ is the $p$-adic closure of the diagonal image of $E$ in the semilocal units $U = \prod_{\mathfrak{P} \mid p} \mathcal{O}_{\mathfrak{P}}^\times$.

The hypothesis says $G \cong (\mathbb{Z}/2)^k$, i.e. $\mathbb{K} = \mathbb{Q}(\sqrt{a_1}, \dots, \sqrt{a_k})$ with all $a_i > 0$, of degree $2^k$ and unit rank $2^k - 1$. This generalises the real quadratic ($k = 1$) and real biquadratic ($k = 2$) cases. It is a special case of Brumer's theorem for abelian fields, but it admits an elementary proof: $\mathbb{K}$ has exactly $2^k - 1$ real quadratic subfields $k_\chi$ (one for each nontrivial character $\chi : G \to \{\pm 1\}$), a suitable power $\eta_\chi$ of the fundamental unit of $k_\chi$ satisfies $\sigma(\eta_\chi) = \eta_\chi^{\chi(\sigma)}$, and operators of the form $u \mapsto u\,\sigma(u)^{\pm 1}$ in $\mathbb{Z}[G]$ separate these eigen-units $p$-adically.

Formalization note. "Multiquadratic" is spelled as IsGalois ℚ K together with ∀ σ : K ≃ₐ[ℚ] K, σ * σ = 1; "totally real" as IsTotallyReal K. The degree is arbitrary (including $\mathbb{K} = \mathbb{Q}$), and no hypothesis on $p$ beyond primality is needed; in particular $p = 2$ is allowed.