The vanishing of the Iwasawa $bc$-invariant for totally real fields

Let $F$ be a totally real field, let $F_{\mathrm{cyc}}$ be its cyclotomic $\mathbb{Z}_p$-extension, and let $M$ be the maximal abelian $p$-extension of $F_{\mathrm{cyc}}$ unramified outside the places over $p$. Then $\operatorname{Gal}(M/F_{\mathrm{cyc}})$ is a finitely generated $\mathbb{Z}_p$-module.

Vanishing of the Iwasawa $\mu$-invariant. For every totally real field $F$, the Galois group over $F_{\mathrm{cyc}}$ of the maximal abelian $p$-extension of $F_{\mathrm{cyc}}$ unramified outside the places over $p$ is a finitely generated $\mathbb{Z}_p$-module.

This is the vanishing of the Iwasawa $\mu$-invariant in the sense used to construct the non-commutative $p$-adic $L$-functions in the paper. The source invokes the weak Leopoldt conjecture to obtain finite generation and explicitly assumes this stronger finite-generation condition; no resolution is supplied here.