English
If q,r ≠ 0 and q+r ≠ 0 and v_p(q) ≤ v_p(r), then v_p(q) ≤ v_p(q+r).
Русский
Пусть q,r ≠ 0 и q+r ≠ 0 и v_p(q) ≤ v_p(r). Тогда v_p(q) ≤ v_p(q+r).
LaTeX
$$$ q \\neq 0 \\land r \\neq 0 \\land q+r \\neq 0 \\land v_p(q) \\le v_p(r) \\Rightarrow v_p(q) \\le v_p(q+r) $$$
Lean4
/-- Sufficient conditions to show that the `p`-adic valuation of `q` is less than or equal to the
`p`-adic valuation of `q + r`. -/
theorem le_padicValRat_add_of_le {q r : ℚ} (hqr : q + r ≠ 0) (h : padicValRat p q ≤ padicValRat p r) :
padicValRat p q ≤ padicValRat p (q + r) :=
if hq : q = 0 then by simpa [hq] using h
else
if hr : r = 0 then by simp [hr]
else by
have hqn : q.num ≠ 0 := Rat.num_ne_zero.2 hq
have hqd : (q.den : ℤ) ≠ 0 := mod_cast Rat.den_nz _
have hrn : r.num ≠ 0 := Rat.num_ne_zero.2 hr
have hrd : (r.den : ℤ) ≠ 0 := mod_cast Rat.den_nz _
have hqreq : q + r = (q.num * r.den + q.den * r.num) /. (q.den * r.den) := Rat.add_num_den _ _
have hqrd : q.num * r.den + q.den * r.num ≠ 0 := Rat.mk_num_ne_zero_of_ne_zero hqr hqreq
conv_lhs => rw [← q.num_divInt_den]
rw [hqreq, padicValRat_le_padicValRat_iff hqn hqrd hqd (mul_ne_zero hqd hrd), ←
emultiplicity_le_emultiplicity_iff, mul_left_comm, emultiplicity_mul (Nat.prime_iff_prime_int.1 hp.1), add_mul]
rw [← q.num_divInt_den, ← r.num_divInt_den, padicValRat_le_padicValRat_iff hqn hrn hqd hrd, ←
emultiplicity_le_emultiplicity_iff] at h
calc
_ ≤ min (emultiplicity (↑p) (q.num * r.den * q.den)) (emultiplicity (↑p) (↑q.den * r.num * ↑q.den)) :=
le_min (by rw [emultiplicity_mul (a := _ * _) (Nat.prime_iff_prime_int.1 hp.1), add_comm])
(by
rw [mul_assoc, emultiplicity_mul (b := _ * _) (Nat.prime_iff_prime_int.1 hp.1)]
exact add_le_add_left h _)
_ ≤ _ := min_le_emultiplicity_add
