English
If x and y are p-adic numbers and x + y ≠ 0, then min(v_p(x), v_p(y)) ≤ v_p(x + y).
Русский
Пусть x, y — числа Рядов p; если x + y ≠ 0, то min(v_p(x), v_p(y)) ≤ v_p(x + y).
LaTeX
$$$\forall x,y\in \mathbb{Q}_p,\ x+y\neq 0\;\Rightarrow\; \min\big(v_p(x),v_p(y)\big) \le v_p(x+y)$$$
Lean4
theorem le_valuation_add {x y : ℚ_[p]} (hxy : x + y ≠ 0) : min x.valuation y.valuation ≤ (x + y).valuation :=
by
by_cases hx : x = 0
· simpa only [hx, zero_add] using min_le_right _ _
by_cases hy : y = 0
· simpa only [hy, add_zero] using min_le_left _ _
have : ‖x + y‖ ≤ max ‖x‖ ‖y‖ := nonarchimedean x y
simpa only [norm_eq_zpow_neg_valuation hxy, norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation hy, le_max_iff,
zpow_le_zpow_iff_right₀ (mod_cast hp.out.one_lt : 1 < (p : ℝ)), neg_le_neg_iff, ← min_le_iff]
