English
For integers n1,n2,d1,d2 with n1,n2,d1,d2 representing nonzero rationals n1/d1 and n2/d2, we have v_p(n1/d1) ≤ v_p(n2/d2) if and only if for all n ∈ N, p^n ∣ (n1 d2) implies p^n ∣ (n2 d1).
Русский
Для целых n1,n2,d1,d2 записывающих дроби n1/d1, n2/d2, выполняется v_p(n1/d1) ≤ v_p(n2/d2) тогда и только тогда, для всех n ∈ N, если p^n делится на n1 d2, то p^n делится на n2 d1.
LaTeX
$$$ (n_1,d_1,n_2,d_2) \\text{ с } n_1,d_1,n_2,d_2 \\in \\mathbb{Z},\\ q_1 = \\dfrac{n_1}{d_1},\\ q_2 = \\dfrac{n_2}{d_2},\\ q_1,q_2 \\neq 0 \\\\ v_p(q_1) \\le v_p(q_2) \\iff \\forall n \\in \\mathbb{N}, \\ (p^n \\mid n_1 d_2) \\Rightarrow (p^n \\mid n_2 d_1) $$$
Lean4
/-- A condition for `padicValRat p (n₁ / d₁) ≤ padicValRat p (n₂ / d₂)`, in terms of
divisibility by `p^n`. -/
theorem padicValRat_le_padicValRat_iff {n₁ n₂ d₁ d₂ : ℤ} (hn₁ : n₁ ≠ 0) (hn₂ : n₂ ≠ 0) (hd₁ : d₁ ≠ 0) (hd₂ : d₂ ≠ 0) :
padicValRat p (n₁ /. d₁) ≤ padicValRat p (n₂ /. d₂) ↔ ∀ n : ℕ, (p : ℤ) ^ n ∣ n₁ * d₂ → (p : ℤ) ^ n ∣ n₂ * d₁ :=
by
have hf1 : FiniteMultiplicity (p : ℤ) (n₁ * d₂) := finite_int_prime_iff.2 (mul_ne_zero hn₁ hd₂)
have hf2 : FiniteMultiplicity (p : ℤ) (n₂ * d₁) := finite_int_prime_iff.2 (mul_ne_zero hn₂ hd₁)
conv =>
lhs
rw [padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₁ hd₁) rfl,
padicValRat.defn p (Rat.divInt_ne_zero_of_ne_zero hn₂ hd₂) rfl, sub_le_iff_le_add', ← add_sub_assoc,
le_sub_iff_add_le]
norm_cast
rw [← multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1) hf1, add_comm, ←
multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1) hf2, hf1.multiplicity_le_multiplicity_iff hf2]
