valuation_inv — Mathlib

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

Похожие утверждения