English
If a rational q has denominator not divisible by p, then the p-adic norm of q is at most 1.
Русский
Если отношение q = a/b имеет знаменатель b не делимый на p, то p-адическая норма q не превосходит 1.
LaTeX
$$$\\forall q\\in\\mathbb{Q},\\ (p\\nmid \\operatorname{den}(q))\\ \\Rightarrow\\ \\|q\\|_p \\le 1$$$
Lean4
theorem norm_rat_le_one : ∀ {q : ℚ} (_ : ¬p ∣ q.den), ‖(q : ℚ_[p])‖ ≤ 1
| ⟨n, d, hn, hd⟩ => fun hq : ¬p ∣ d ↦
if hnz : n = 0 then by
have : (⟨n, d, hn, hd⟩ : ℚ) = 0 := Rat.zero_iff_num_zero.mpr hnz
norm_num [this]
else by
have hnz' : (⟨n, d, hn, hd⟩ : ℚ) ≠ 0 := mt Rat.zero_iff_num_zero.1 hnz
rw [eq_padicNorm]
norm_cast
-- Porting note: `Nat.cast_zero` instead of another `norm_cast` call
rw [padicNorm.eq_zpow_of_nonzero hnz', padicValRat, neg_sub, padicValNat.eq_zero_of_not_dvd hq, Nat.cast_zero,
zero_sub, zpow_neg, zpow_natCast]
apply inv_le_one_of_one_le₀
norm_cast
apply one_le_pow
exact hp.1.pos
