Facts about the adic topology and local fields

theorem IsNonarchimedeanLocalField.maximalIdeal_pow_eq (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (n : ℕ) : ↑(IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer ^ n) = Subtype.val ⁻¹' {x : K | (ValuativeRel.valuation K) x ≤ (valueGroupWithZeroIsoInt K).symm (WithZero.exp (-↑n))}

theorem IsNonarchimedeanLocalField.isAdic (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : IsAdic (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer)

instance IsNonarchimedeanLocalField.instIsAdicCompleteSubtypeMemSubringIntegerValueGroupWithZeroValuationMaximalIdeal_classFieldTheory (K : Type u_1) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : IsAdicComplete (IsLocalRing.maximalIdeal ↥(ValuativeRel.valuation K).integer) ↥(ValuativeRel.valuation K).integer