norm_lt_one_iff_dvd — Mathlib

English

For any x ∈ ℤ_p, the p-adic norm satisfies ||x|| < 1 if and only if p divides x.

Русский

Для любого x ∈ ℤ_p p-адическая норма удовлетворяет ||x|| < 1 тогда и только тогда, когда p делит x.

LaTeX

$$$\forall x\in \mathbb{Z}_p,\ \|x\| < 1 \iff p \;|\; x.$$

Lean4

theorem norm_lt_one_iff_dvd (x : ℤ_[p]) : ‖x‖ < 1 ↔ ↑p ∣ x :=
  by
  have := norm_le_pow_iff_mem_span_pow x 1
  rw [Ideal.mem_span_singleton, pow_one] at this
  rw [← this, norm_le_pow_iff_norm_lt_pow_add_one]
  simp only [zpow_zero, Int.ofNat_zero, Int.natCast_succ, neg_add_cancel, zero_add]

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