Theorems · Theorem · number theory
PadicInt.coe_adicCompletionIntegersEquiv_symm_apply
∀ (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) (x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ (Rat.HeightOneSpectrum.primesEquiv.symm p))), ↑((PadicInt.adicCompletionIntegersEquiv R p).symm x) = (Padic.adicCompletionEquiv R p).symm ↑x
The diagram
``
ℤ_[p] < -- (primesEquiv.symm p).adicCompletionIntegers ℚ
| |
| |
v v
ℚ_[p] < -- (primesEquiv.symm p).adicCompletion ℚ
``
commutes.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 189 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites32
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
- Realstatement · cited by 25,697
- CommRingstatement and proof · cited by 17,173
- Algebrastatement and proof · cited by 11,388
- Equivstatement · cited by 8,337
- Norm.normstatement and proof · cited by 5,413
- 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
- Equiv.apply_symm_applyproof · cited by 346
- IsDedekindDomain.HeightOneSpectrumstatement · cited by 338
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.