Theorems · Theorem · number theory

Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply

∀ {R : Type u_2} [inst : CommRing R] [inst_1 : Algebra R ℚ] [inst_2 : IsIntegralClosure R ℤ ℚ]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R ℚ] (v : IsDedekindDomain.HeightOneSpectrum R)
  (x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ v)),
  ↑((Rat.HeightOneSpectrum.adicCompletionIntegers.padicIntEquiv v) x) =
    (Rat.HeightOneSpectrum.adicCompletion.padicEquiv v) ↑x

The diagram `` v.adicCompletionIntegers ℚ --> ℤ_[primesEquiv v] | | | | v v v.adicCompletion ℚ -> ℚ_[primesEquiv v] `` commutes.

Defined in

Mathlib.NumberTheory.Padics.HeightOneSpectrum

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAlgebraIsIntegralClosureIsDedekindDomainIsFractionRing