Leopoldt's conjecture for totally real biquadratic fields

Leopoldt's conjecture holds, at every prime $p$, for every totally real biquadratic field: if $\mathbb{K}$ is totally real, Galois over $\mathbb{Q}$ of degree $4$, and every element of $G = \mathrm{Gal}(\mathbb{K}/\mathbb{Q})$ satisfies $\sigma^2 = 1$ (so $G \cong (\mathbb{Z}/2)^2$ and $\mathbb{K} = \mathbb{Q}(\sqrt{a},\sqrt{b})$ with $a, b > 0$), then

Here $E = \mathcal{O}_{\mathbb{K}}^\times$ has $\mathbb{Z}$-rank $4 - 1 = 3$, 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$.

This is the unit-rank-$3$ case of Brumer's theorem (Leopoldt's conjecture for abelian fields), the first case beyond unit rank $1$ where the conjecture has genuine content for totally real fields. The units of the three real quadratic subfields $k_1, k_2, k_3$ generate a subgroup of finite index in $E$, and the Galois group acts on each of them through a distinct character; this eigenspace decomposition is what makes the biquadratic case accessible by elementary means, without Baker's theory of linear forms in $p$-adic logarithms.

Formalization note. "Biquadratic" is spelled as IsGalois ℚ K, $[\mathbb{K}:\mathbb{Q}] = 4$ and ∀ σ : K ≃ₐ[ℚ] K, σ * σ = 1, and "totally real" as IsTotallyReal K. No hypothesis on $p$ beyond primality is needed. In particular $p = 2$ is allowed.