norm_le_one_iff_val_nonneg — Mathlib

English

The p-adic norm is ≤ 1 iff the valuation is ≥ 0.

Русский

Падикова нормa не больше единицы тогда и только когда оценка неотрицательна.

LaTeX

$$‖x‖ ≤ 1 \Leftrightarrow 0 \le v_p(x)$$

Lean4

theorem norm_le_one_iff_val_nonneg (x : ℚ_[p]) : ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation :=
  by
  by_cases hx : x = 0
  · simp only [hx, norm_zero, valuation_zero, zero_le_one, le_refl]
  · rw [norm_eq_zpow_neg_valuation hx, ← zpow_zero (p : ℝ), zpow_le_zpow_iff_right₀, neg_nonpos]
    exact Nat.one_lt_cast.2 (Nat.Prime.one_lt' p).1

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