Theorems · Definition · number theory

Padic.adicCompletionEquiv

(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.adicCompletion ℚ (Rat.HeightOneSpectrum.primesEquiv.symm p)

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

Defined in: Mathlib.NumberTheory.Padics.HeightOneSpectrum
Cited by: 2 results in Mathlib
Foundations: Depth 173 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing IsDedekindDomain Algebra IsFractionRing IsIntegralClosure

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites19

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
CommRingstatement and proof · cited by 17,173
Algebrastatement and proof · cited by 11,388
Equivstatement · cited by 8,337
Equiv.symmstatement and proof · cited by 3,681
Nat.Primestatement · cited by 2,059
IsFractionRingstatement and proof · cited by 738
IsDedekindDomainstatement and proof · cited by 668
IsDedekindDomain.HeightOneSpectrumstatement · cited by 338
Padicstatement · cited by 151
IsIntegralClosurestatement and proof · cited by 146
ContinuousAlgEquivstatement · cited by 105

Cited by2

Results whose statement or proof uses this declaration.

PadicInt.coe_adicCompletionIntegersEquiv_applystatement · cited by 0
PadicInt.coe_adicCompletionIntegersEquiv_symm_applystatement · cited by 0