Unramified Iwasawa torsion theorem (source code)

= Unramified Iwasawa torsion theorem
{title2=$\operatorname{rank}_\Lambda Y=0$}

The <unramified Iwasawa module> is finitely generated torsion over the <Iwasawa algebra of a Zp-extension>, for every <Zp-extension> of a <number field>. After a finite shift all ramified primes are totally ramified and their number $s$ is constant. <Class field theory> bounds finite-layer <coinvariant modules> by $\operatorname{rank}_{\mathbb Z_p}Y_{\Gamma_n}\leq s-1$. The <Compact Nakayama lemma> proves finite generation, and a positive <Iwasawa-module rank> would force ranks at least $r p^n$, a contradiction. No <Leopoldt conjecture> is required.