norm_int_le_pow_iff_dvd — Mathlib

English

For k ∈ ℤ and n ∈ ℕ, ‖k‖_p ≤ p^{-n} iff p^{n} ∣ k.

Русский

Для k ∈ ℤ и n ∈ ℕ, ‖k‖_p ≤ p^{-n} тогда и только тогда, когда p^{n} делит k.

LaTeX

$$$‖k‖_p ≤ p^{-n} \\iff p^{n} \\mid k$$$

Lean4

theorem norm_int_le_pow_iff_dvd (k : ℤ) (n : ℕ) : ‖(k : ℚ_[p])‖ ≤ (p : ℝ) ^ (-n : ℤ) ↔ (p ^ n : ℤ) ∣ k :=
  by
  have : (p : ℝ) ^ (-n : ℤ) = (p : ℚ) ^ (-n : ℤ) := by simp
  rw [show (k : ℚ_[p]) = ((k : ℚ) : ℚ_[p]) by norm_cast, eq_padicNorm, this]
  norm_cast
  rw [← padicNorm.dvd_iff_norm_le]

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