Growth of class group of ℤₚ-extension of number fields

theorem MvZpExtension.multiplicity_classNumber_Kn_eq₁ {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [NumberField K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) [Unique ι] : ∃ (mu : ℕ) (lambda : ℕ) (nu : ℕ) (N : ℕ), ∀ n > N, multiplicity (NumberField.classNumber ↥(H.Kn n)) p = mu * p ^ n + lambda * p + nu

Iwasawa's theorem on growth of class groups of ℤₚ-extension of number fields.

theorem IsMvZpExtension.multiplicity_classNumber_Kn_eq₁ {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_2} {Kinf : Type u_3} [Field K] [NumberField K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p 1 K Kinf) : ∃ (mu : ℕ) (lambda : ℕ) (nu : ℕ) (N : ℕ), ∀ n > N, multiplicity (NumberField.classNumber ↥(H.Kn n)) p = mu * p ^ n + lambda * p + nu

Iwasawa's theorem on growth of class groups of ℤₚ-extension of number fields.