norm_le_pow_iff_mem_span_pow — Mathlib

English

For any x in Z_p and n ∈ N, ||x|| ≤ p^{−n} if and only if x belongs to the span of p^n, i.e., x ∈ (p^n)Z_p.

Русский

Для любого x в Z_p и n ∈ N, выполняется равноcть ||x|| ≤ p^{−n} тогда и только тогда, когда x принадлежит порожденному p^n идеалу: x ∈ (p^n)Z_p.

LaTeX

$$$\forall x\in \mathbb{Z}_p,\forall n\in\mathbb{N},\ \|x\| \le p^{-n} \iff x \in (p^n)\mathbb{Z}_p.$$$

Lean4

theorem norm_le_pow_iff_mem_span_pow (x : ℤ_[p]) (n : ℕ) :
    ‖x‖ ≤ (p : ℝ) ^ (-n : ℤ) ↔ x ∈ (Ideal.span {(p : ℤ_[p]) ^ n} : Ideal ℤ_[p]) :=
  by
  by_cases hx : x = 0
  · subst hx
    simp only [norm_zero, zpow_neg, zpow_natCast, inv_nonneg, iff_true, Submodule.zero_mem]
    exact mod_cast Nat.zero_le _
  rw [norm_le_pow_iff_le_valuation x hx, mem_span_pow_iff_le_valuation x hx]

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