Theorems · Definition · number theory
padicNormE
{p : ℕ} → [hp : Fact (Nat.Prime p)] → AbsoluteValue ℚ_[p] ℚThe rational-valued p-adic norm on ℚ_[p] is lifted from the norm on Cauchy sequences. The
canonical form of this function is the normed space instance, with notation ‖ ‖.
- Defined in
- Mathlib.NumberTheory.Padics.PadicNumbers
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Fact
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- AbsoluteValuestatement · cited by 363
- Padicstatement and proof · cited by 151
- PadicSeq.normproof · cited by 20
- PadicSeq.norm_equivproof · cited by 4
Cited by19
Results whose statement or proof uses this declaration.
- Padic.eq_padicNormproof · cited by 6
- Padic.add_eq_max_of_neproof · cited by 4
- Padic.nonarchimedeanproof · cited by 4
- padicNormE.defnstatement · cited by 3
- padicNormE.eq_padic_norm'statement · cited by 3
- Padic.limSeqstatement and proof · cited by 3
- Padic.rat_denseproof · cited by 2
- Padic.rat_dense'statement and proof · cited by 2
- Padic.exi_rat_seq_convstatement and proof · cited by 2
- Padic.padicNormE.mulproof · cited by 2
- Padic.complete'statement and proof · cited by 1
- padicNormE.add_eq_max_of_ne'statement · cited by 1