Theorems · Definition · number theory
Padic
(p : ℕ) → [Fact (Nat.Prime p)] → Type
The p-adic numbers ℚ_[p] are the Cauchy completion of ℚ with respect to the p-adic norm.
- Defined in
- Mathlib.NumberTheory.Padics.PadicNumbers
- Cited by
- 151 results in Mathlib
- Foundations
- Depth 86 from the axioms, rests on 2,315 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- Fact
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Factstatement and proof · cited by 2,726
- Nat.Primestatement and proof · cited by 2,059
- padicNormproof · cited by 83
- CauSeq.Completion.Cauchyproof · cited by 62
Cited by171
Results whose statement or proof uses this declaration.
- PadicIntproof · cited by 179
- Padic.valuationstatement · cited by 28
- PadicAlgClproof · cited by 21
- padicNormEstatement and proof · cited by 18
- PadicInt.unitCoeffproof · cited by 9
- Padic.norm_eq_zpow_neg_valuationstatement and proof · cited by 9
- Padic.eq_padicNormstatement · cited by 6
- Padic.mulValuationstatement and proof · cited by 6
- Padic.valuation_natCaststatement and proof · cited by 6
- PadicInt.norm_defstatement · cited by 5
- Rat.HeightOneSpectrum.adicCompletion.padicEquivstatement and proof · cited by 5
- Padic.mkstatement · cited by 5