13. Iwasawa mu-invariant
We close the formalisation with classical Iwasawa theory: the \mu- and
\lambda-invariants of a \Zp-extension. Proving Iwasawa's growth formula for
class numbers develops exactly the tools needed to see that the Galois modules
appearing in the Jacinto and Williams (2023) theory are finitely generated torsion
\Lam-modules — the algebraic input to the Iwasawa Main Conjecture beyond the
Vandiver case. Throughout, p is a fixed prime and F a number field.