Theorems · Theorem · number theory
PadicInt.coe_adicCompletionIntegersEquiv_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 : ℤ_[↑p]), ↑((PadicInt.adicCompletionIntegersEquiv R p) x) = (Padic.adicCompletionEquiv R p) ↑x
The diagram
``
ℤ_[p] --> (primesEquiv.symm p).adicCompletionIntegers ℚ
| |
| |
v v
ℚ_[p] --> (primesEquiv.symm p).adicCompletion ℚ
``
commutes.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 188 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites26
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.