Growth of class group of ℤₚ-extension of number fields #
theorem
IsZpExtension.multiplicity_classNumber_Kn_eq
{p : ℕ}
[Fact (Nat.Prime p)]
{K : Type u}
{Kinf : Type v}
[Field K]
[NumberField K]
[Field Kinf]
[Algebra K Kinf]
[IsGalois K Kinf]
(H : IsZpExtension p K Kinf)
:
∃ (mu : ℕ) (lambda : ℕ) (nu : ℕ) (N : ℕ),
∀ n > N, multiplicity (NumberField.classNumber ↥(IsMvZpExtension.Kn H n)) p = mu * p ^ n + lambda * p + nu
Iwasawa's theorem on growth of class groups of ℤₚ-extension
of number fields.