ofIntSeq — Mathlib

English

For any x in ℤ_p, (x : ℚ_p) = 0 iff x = 0.

Русский

Для любого x ∈ ℤ_p, (x : ℚ_p) = 0 тогда и только тогда, когда x = 0.

LaTeX

$$$(x : \mathbb{Q}_p) = 0 \iff x = 0$$$

Lean4

/-- A sequence of integers that is Cauchy with respect to the `p`-adic norm converges to a `p`-adic
integer. -/
def ofIntSeq (seq : ℕ → ℤ) (h : IsCauSeq (padicNorm p) fun n => seq n) : ℤ_[p] :=
  ⟨⟦⟨_, h⟩⟧,
    show ↑(PadicSeq.norm _) ≤ (1 : ℝ) by
      rw [PadicSeq.norm]
      split_ifs with hne <;> norm_cast
      apply padicNorm.of_int⟩

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