English
If q,r are nonzero and v_p(q) ≠ v_p(r) and q+r ≠ 0, then v_p(q+r) = min(v_p(q), v_p(r)) under appropriate nonzero-valuation conditions.
Русский
Если q,r ненулевые и v_p(q) ≠ v_p(r) и q+r ≠ 0, то при подходящих условиях учёта ненулевых значений выполняется v_p(q+r) = min(v_p(q), v_p(r)).
LaTeX
$$$ q,r \\neq 0 \\land v_p(q) \\neq v_p(r) \\land q+r \\neq 0 \\Rightarrow v_p(q+r) = \\min\\{v_p(q), v_p(r)\\} $$$
Lean4
/-- Ultrametric property of a p-adic valuation. -/
theorem add_eq_min {q r : ℚ} (hqr : q + r ≠ 0) (hq : q ≠ 0) (hr : r ≠ 0) (hval : padicValRat p q ≠ padicValRat p r) :
padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r) :=
by
have h1 := min_le_padicValRat_add (p := p) hqr
have h2 := min_le_padicValRat_add (p := p) (ne_of_eq_of_ne (add_neg_cancel_right q r) hq)
have h3 := min_le_padicValRat_add (p := p) (ne_of_eq_of_ne (add_neg_cancel_right r q) hr)
rw [add_neg_cancel_right, padicValRat.neg] at h2 h3
rw [add_comm] at h3
omega
