English
For any rational x, v_p(x) ≤ 1 if and only if p does not divide the denominator of x (in lowest terms).
Русский
Для любой дроби x v_p(x) ≤ 1 тогда и только тогда, когда p не делит знаменатель x в несжатой форме.
LaTeX
$$v_p(x) \\le 1 \\Leftrightarrow p \\nmid \\mathrm{den}(x)$$
Lean4
theorem padicValuation_le_one_iff {p : ℕ} [Fact p.Prime] {x : ℚ} : Rat.padicValuation p x ≤ 1 ↔ ¬p ∣ x.den :=
by
nth_rw 1 [← x.num_div_den, map_div₀, ← Int.natCast_dvd_natCast, ← Int.padicValuation_eq_one_iff,
Rat.padicValuation_cast, ← Int.cast_natCast, Rat.padicValuation_cast, div_le_one₀]
· rcases (Int.padicValuation_le_one p x.den).eq_or_lt with h | h
· simp [h, Int.padicValuation_le_one]
· simp only [h.ne, iff_false, not_le]
rcases (Int.padicValuation_le_one p x.num).eq_or_lt with h' | h'
· simp [h, h']
· rw [Int.padicValuation_lt_one_iff] at h h'
exfalso
rw [Int.natCast_dvd_natCast] at h
rw [Int.natCast_dvd] at h'
exact Nat.not_coprime_of_dvd_of_dvd (Nat.Prime.one_lt Fact.out) h h' x.reduced.symm
· simp [zero_lt_iff]
