English
The p-adic valuation on ℚ_p is extended to a valuation mulValuation with values in a topological monoid, defined by toFun x = if x = 0 then 0 else exp(-v_p(x)).
Русский
Падикова оценка упрощена в валюацию mulValuation: toFun(x) = 0 при x=0, иначе exp(−v_p(x)).
LaTeX
$$mulValuation(x) = \begin{cases} 0, & x=0, \\ \exp(-v_p(x)), & x\neq 0 \end{cases}$$
Lean4
/-- The `p`-adic valuation on `ℚ_[p]`, as a `Valuation`, bundled `Padic.valuation`. -/
@[simps]
noncomputable def mulValuation : Valuation ℚ_[p] ℤᵐ⁰
where
toFun x := if x = 0 then 0 else exp (-x.valuation)
map_zero' := by simp
map_one' := by simp
map_mul' _ _ := by split_ifs <;> simp_all [add_comm]
map_add_le_max' _
_ := by
split_ifs
any_goals simp_all [inv_le_inv₀]
simpa using le_valuation_add ‹_›
