 Leopoldt theorem for abelian number fields

The Leopoldt conjecture holds for every finite abelian extension of $\mathbb{Q}$. The proof uses linear independence of $p$-adic logarithms of algebraic numbers. In cyclotomic towers it supplies the ranks of the global-unit terms in the class-field unit sequence; it is not needed for the unramified Iwasawa torsion theorem in arbitrary towers.