English
For any p-adic number x, v_p(x^{-1}) = −v_p(x).
Русский
Для любого p-числа x выполняется v_p(x^{-1}) = −v_p(x).
LaTeX
$$$v_p(x^{-1}) = -v_p(x)$$
Lean4
@[simp]
theorem valuation_inv (x : ℚ_[p]) : x⁻¹.valuation = -x.valuation :=
by
obtain rfl | hx := eq_or_ne x 0
· simp
have h_norm : ‖x⁻¹‖ = ‖x‖⁻¹ := norm_inv x
have hp_ne_one : (p : ℝ) ≠ 1 := mod_cast (Fact.out : p.Prime).ne_one
have hp_pos : (0 : ℝ) < p := mod_cast NeZero.pos _
rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation <| inv_ne_zero hx, ← zpow_neg,
zpow_right_inj₀ hp_pos hp_ne_one, neg_inj] at h_norm