English
For a prime p, the p-adic valuation on rationals is the valuation v_p: ℚ → ℤᵐ⁰ defined by v_p(x) = 0 if x = 0, and v_p(x) = exp(-padicValRat p x) otherwise. This map satisfies the axioms of a valuation.
Русский
Для простого p p-адическая валюация на рациональных числах задаётся как v_p(x) = 0, если x = 0; иначе v_p(x) = exp(-padicValRat p x). Это отображение удовлетворяет аксиомам вальюации.
LaTeX
$$$v_p:\\mathbb{Q}\\to \\mathbb{Z}_{\\ge 0}^{\\infty} \\text{ (extended multiplicative monoid)}\\quad\\text{defined by } v_p(x)=\\begin{cases}0,& x=0,\\\\ e^{-\\mathrm{padicVal}_p(x)},& x\\neq 0,\\end{cases}$$$
Lean4
/-- The p-adic valuation on rationals, sending `p` to `(exp (-1) : ℤᵐ⁰)` -/
def padicValuation (p : ℕ) [Fact p.Prime] : Valuation ℚ ℤᵐ⁰
where
toFun x := if x = 0 then 0 else exp (-padicValRat p x)
map_zero' := by simp
map_one' := by simp
map_mul' := by
intros
split_ifs <;> simp_all [padicValRat.mul, exp_add, mul_comm]
map_add_le_max' := by
intros
split_ifs
any_goals simp_all [-exp_neg]
rw [← min_le_iff]
exact padicValRat.min_le_padicValRat_add ‹_›
