English
For any natural n and integer z, p^n divides z if and only if padicNorm p z ≤ (p)^{-n} in ℚ.
Русский
Для любого натурального n и целого z: p^n делит z тогда и только тогда, когда padicNorm p z ≤ p^{-n} в ℚ.
LaTeX
$$$ \uparrow(p^n) \mid z \;\iff\; padicNorm\ p\ z \le (p: \mathbb{Q})^{-n} $$$
Lean4
theorem dvd_iff_norm_le {n : ℕ} {z : ℤ} : ↑(p ^ n) ∣ z ↔ padicNorm p z ≤ (p : ℚ) ^ (-n : ℤ) :=
by
unfold padicNorm; split_ifs with hz
· norm_cast at hz
simp [hz]
· rw [zpow_le_zpow_iff_right₀, neg_le_neg_iff, padicValRat.of_int, padicValInt.of_ne_one_ne_zero hp.1.ne_one _]
· norm_cast
rw [← FiniteMultiplicity.pow_dvd_iff_le_multiplicity]
· norm_cast
· apply Int.finiteMultiplicity_iff.2 ⟨by simp [hp.out.ne_one], mod_cast hz⟩
· exact_mod_cast hz
· exact_mod_cast hp.out.one_lt
