English
The minimum of the valuations of q and r is not greater than the valuation of q+r: min(v_p(q), v_p(r)) ≤ v_p(q+r).
Русский
Минимум v_p(q) и v_p(r) не превосходит v_p(q+r).
LaTeX
$$$ q,r \\neq 0 \\Rightarrow \\min\\{v_p(q), v_p(r)\\} \\le v_p(q+r) $$$
Lean4
/-- The minimum of the valuations of `q` and `r` is at most the valuation of `q + r`. -/
theorem min_le_padicValRat_add {q r : ℚ} (hqr : q + r ≠ 0) :
min (padicValRat p q) (padicValRat p r) ≤ padicValRat p (q + r) :=
(le_total (padicValRat p q) (padicValRat p r)).elim
(fun h => by rw [min_eq_left h]; exact le_padicValRat_add_of_le hqr h)
(fun h => by rw [min_eq_right h, add_comm]; exact le_padicValRat_add_of_le (by rwa [add_comm]) h)