English
Definition: for a prime p, padic(p) is the p-adic absolute value on Q valued in R.
Русский
Определение: для простого p, padic(p) — p-адическое абсолютное значение на Q, принимает значения в R.
LaTeX
$$def padic (p) : AbsoluteValue ℚ ℝ$$
Lean4
/-- The real-valued `AbsoluteValue` corresponding to the p-adic norm on `ℚ`. -/
def padic (p : ℕ) [Fact p.Prime] : AbsoluteValue ℚ ℝ
where
toFun x := (padicNorm p x : ℝ)
map_mul' := by simp only [padicNorm.mul, Rat.cast_mul, forall_const]
nonneg' x := cast_nonneg.mpr <| padicNorm.nonneg x
eq_zero'
x :=
⟨fun H ↦ padicNorm.zero_of_padicNorm_eq_zero <| cast_eq_zero.mp H, fun H ↦
cast_eq_zero.mpr <| H ▸ padicNorm.zero (p := p)⟩
add_le' x y := by exact_mod_cast padicNorm.triangle_ineq x y
