ℤₚ-extension of number fields #
instance
MvZpExtension.numberField_Kn
{p : ℕ}
[Fact (Nat.Prime p)]
{ι : Type u_1}
{K : Type u_2}
{Kinf : Type u_3}
[Finite ι]
[Field K]
[Field Kinf]
[Algebra K Kinf]
[IsGalois K Kinf]
(H : MvZpExtension p ι K Kinf)
[NumberField K]
(n : ℕ)
:
NumberField ↥(H.Kn n)
instance
IsMvZpExtension.numberField_Kn
{p : ℕ}
[Fact (Nat.Prime p)]
{d : ℕ}
{K : Type u_2}
{Kinf : Type u_3}
[Field K]
[Field Kinf]
[Algebra K Kinf]
[IsGalois K Kinf]
(H : IsMvZpExtension p d K Kinf)
[NumberField K]
(n : ℕ)
:
NumberField ↥(H.Kn n)