1 Introduction
1.1 Iwasawa’s theorem on growth of class groups
The first goal of this project is formalize the proof of Iwasawa’s theorem on growth of class groups in a \({\mathbb {Z}}_p\)-extension tower in LꓱꓯN.
Let \(K\) be a field, \(p\) be a prime.
(i) An extension \(K_\infty /K\) is called a \({\mathbb {Z}}_p\)-extension, if it is Galois with \(\Gamma ={\mathrm{Gal}}(K_\infty /K)\cong {\mathbb {Z}}_p\) as topological groups.
(ii) If \(K_\infty /K\) is a \({\mathbb {Z}}_p\)-extension, then for any \(n\geq 0\), define \(K_n:=K_\infty ^{\Gamma ^{p^n}}\).
Let \(K\) be a number field, \(p\) be a prime, \(K_\infty /K\) be a \({\mathbb {Z}}_p\)-extension. Then there exist integers \(\lambda ,\mu ,\nu \) such that for all sufficiently large \(n\), \(\operatorname{ord}_p(\# {\mathrm{Cl}}(K_n))=\mu p^n+\lambda n+\nu \).