Completion of a number field at a finite place

instance NumberField.instFiniteResidueFieldAdicCompletionIntegers (K : Type u_1) [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) : Finite (IsLocalRing.ResidueField ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v))

instance instFiniteResidueFieldAdicCompletionRingOfIntegersWithZeroMultiplicativeInt_fLT (K : Type u_1) [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : Finite (Valued.ResidueField (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v))

instance NumberField.instCompactSpaceAdicCompletionIntegers (K : Type u_1) [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) : CompactSpace ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)

theorem NumberField.isOpenAdicCompletionIntegers (K : Type u_1) [Field K] [NumberField K] (v : IsDedekindDomain.HeightOneSpectrum (RingOfIntegers K)) : IsOpen ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)