ℤₚ-extension of number fields

instance IsMvZpExtension.charZero_Kn {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) [CharZero K] (n : ℕ) : CharZero ↥(H.Kn n)

instance IsMvZpExtension.numberField_Kn {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u} {Kinf : Type v} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) [NumberField K] (n : ℕ) : NumberField ↥(H.Kn n)