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 p (NumberField.classNumber ↥(H.Kn n))) = ↑mu * ↑p ^ n + ↑lambda * ↑p + nu

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