norm_int_le_pow_iff_dvd — Mathlib

English

For integers viewed inside Z_p, the inequality ∥k∥ ≤ p^{−n} is equivalent to p^{n} dividing k, for k ∈ Z.

Русский

Для целых k, рассматриваемых как элементы Z_p, неравенство ∥k∥ ≤ p^{−n} эквивалентно тому, что p^{n} делит k.

LaTeX

$$$$\|k\| \le p^{-n} \iff p^{n} \mid k.$$$$

Lean4

theorem norm_int_le_pow_iff_dvd {k : ℤ} {n : ℕ} : ‖(k : ℤ_[p])‖ ≤ (p : ℝ) ^ (-n : ℤ) ↔ (p ^ n : ℤ) ∣ k :=
  suffices ‖(k : ℚ_[p])‖ ≤ (p : ℝ) ^ (-n : ℤ) ↔ (p ^ n : ℤ) ∣ k by simpa [norm_intCast_eq_padic_norm]
  Padic.norm_int_le_pow_iff_dvd _ _

Похожие утверждения