English
Constant spectra of padic norm distinguish rationals: const(padicNorm p)(q) ≈ const(padicNorm p)(r) iff q = r.
Русский
Постоянные спектры p-адической нормы различают рациональные числа: const(padicNorm p)(q) ≈ const(padicNorm p)(r) эквивалентно q = r.
LaTeX
$$$\\operatorname{const}(\\mathrm{padicNorm}_p)(q) \\approx \\operatorname{const}(\\mathrm{padicNorm}_p)(r) \\iff q = r$$$
Lean4
/-- 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 `‖ ‖`. -/
def padicNormE {p : ℕ} [hp : Fact p.Prime] : AbsoluteValue ℚ_[p] ℚ
where
toFun := Quotient.lift PadicSeq.norm <| @PadicSeq.norm_equiv _ _
map_mul' q r := Quotient.inductionOn₂ q r <| PadicSeq.norm_mul
nonneg' q := Quotient.inductionOn q <| PadicSeq.norm_nonneg
eq_zero'
q :=
Quotient.inductionOn q fun r ↦ by
rw [Padic.zero_def, Quotient.eq]
exact PadicSeq.norm_zero_iff r
add_le' q
r :=
by
trans
max ((Quotient.lift PadicSeq.norm <| @PadicSeq.norm_equiv _ _) q)
((Quotient.lift PadicSeq.norm <| @PadicSeq.norm_equiv _ _) r)
· exact Quotient.inductionOn₂ q r <| PadicSeq.norm_nonarchimedean
refine max_le_add_of_nonneg (Quotient.inductionOn q <| PadicSeq.norm_nonneg) ?_
exact Quotient.inductionOn r <| PadicSeq.norm_nonneg
