norm_le_pow_iff_le_valuation — Mathlib

English

For any nonzero x in Z_p and any natural number n, the p-adic norm satisfies ||x|| ≤ p^{−n} if and only if n ≤ v_p(x), where v_p(x) is the p-adic valuation.

Русский

Для любого ненулевого x в Z_p и любого натурального n выполняется неравенство ||x|| ≤ p^{−n} тогда и только тогда, когда n ≤ v_p(x), где v_p(x) — p-адическая валюация x.

LaTeX

$$$\forall x \in \mathbb{Z}_p\setminus\{0\},\ \forall n\in\mathbb{N},\ \|x\| \le p^{-n} \iff n \le v_p(x).$$$

Lean4

theorem norm_le_pow_iff_le_valuation (x : ℤ_[p]) (hx : x ≠ 0) (n : ℕ) : ‖x‖ ≤ (p : ℝ) ^ (-n : ℤ) ↔ n ≤ x.valuation :=
  by
  rw [norm_eq_zpow_neg_valuation hx, zpow_le_zpow_iff_right₀, neg_le_neg_iff, Nat.cast_le]
  exact mod_cast hp.out.one_lt

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