valuation_coe_nonneg — Mathlib

English

For every x in the p-adic integers, the p-adic valuation of x (computed in the rational field) is nonnegative.

Русский

Для каждого x из ℤ_p п-adическая ценность x (вычисляемая в поле Q_p) неотрицательна.

LaTeX

$$0 \le (x : \mathbb{Q}_{p}).valuation$$

Lean4

theorem valuation_coe_nonneg : 0 ≤ (x : ℚ_[p]).valuation :=
  by
  obtain rfl | hx := eq_or_ne x 0
  · simp
  have := x.2
  rwa [Padic.norm_eq_zpow_neg_valuation <| coe_ne_zero.2 hx, zpow_le_one_iff_right₀, neg_nonpos] at this
  exact mod_cast hp.out.one_lt

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