norm_le_pow_iff_norm_lt_pow_add_one

English

For all x ∈ Z_p and integer n, the inequalities ||x|| ≤ p^{n} and ||x|| < p^{n+1} are equivalent, i.e., ||x|| ≤ p^{n} iff ||x|| < p^{n+1}.

Русский

Для любого x в Z_p и целого n верно: ||x|| ≤ p^{n} тогда и только тогда, когда ||x|| < p^{n+1}.

LaTeX

$$$\forall x\in \mathbb{Z}_p,\ n\in \mathbb{Z},\ \|x\| \le p^{n} \iff \|x\| < p^{n+1}.$$$

Lean4

theorem norm_le_pow_iff_norm_lt_pow_add_one (x : ℤ_[p]) (n : ℤ) : ‖x‖ ≤ (p : ℝ) ^ n ↔ ‖x‖ < (p : ℝ) ^ (n + 1) := by
  rw [norm_def]; exact Padic.norm_le_pow_iff_norm_lt_pow_add_one _ _

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