Theorems · Definition · number theory

PadicInt.adicCompletionIntegersEquiv

(R : Type u_2) →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      [inst_2 : Algebra R ℚ] →
        [inst_3 : IsFractionRing R ℚ] →
          [inst_4 : IsIntegralClosure R ℤ ℚ] →
            (p : Nat.Primes) →
              ℤ_[↑p] ≃A[ℤ]
                ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ
                    (Rat.HeightOneSpectrum.primesEquiv.symm p))

The continuous ℤ-algebra isomorphism between ℤ_[p] and (primesEquiv.symm p).adicCompletionIntegers ℚ.

Defined in

Mathlib.NumberTheory.Padics.HeightOneSpectrum

Cited by

2 results in Mathlib

Foundations

Depth 187 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsDedekindDomainAlgebraIsFractionRingIsIntegralClosure