norm_lt_pow_iff_norm_le_pow_sub_one

English

For all x ∈ Z_p and n ∈ Z, ||x|| < p^{n} if and only if ||x|| ≤ p^{n-1}.

Русский

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

LaTeX

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

Lean4

theorem norm_lt_pow_iff_norm_le_pow_sub_one (x : ℤ_[p]) (n : ℤ) : ‖x‖ < (p : ℝ) ^ n ↔ ‖x‖ ≤ (p : ℝ) ^ (n - 1) := by
  rw [norm_le_pow_iff_norm_lt_pow_add_one, sub_add_cancel]

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