inv — Mathlib

English

For any q ≠ 0, the p-adic valuation of the inverse equals the negation of the valuation: v_p(q^{-1}) = −v_p(q).

Русский

Для любого q ≠ 0 верно: v_p(q^{-1}) = −v_p(q).

LaTeX

$$$ q \\neq 0 \\Rightarrow v_p(q^{-1}) = -\,v_p(q) $$$

Lean4

/-- A rewrite lemma for `padicValRat p (q⁻¹)` with condition `q ≠ 0`. -/
protected theorem inv (q : ℚ) : padicValRat p q⁻¹ = -padicValRat p q :=
  by
  by_cases hq : q = 0
  · simp [hq]
  · rw [eq_neg_iff_add_eq_zero, ← padicValRat.mul (inv_ne_zero hq) hq, inv_mul_cancel₀ hq, padicValRat.one]

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