Theorems · Theorem · number theory

PadicSeq.stationary

∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {f : CauSeq ℚ (padicNorm p)},
  ¬f ≈ 0 → ∃ N, ∀ (m n : ℕ), N ≤ m → N ≤ n → padicNorm p (↑f n) = padicNorm p (↑f m)

The p-adic norm of the entries of a nonzero Cauchy sequence of rationals is eventually constant.

Defined in

Mathlib.NumberTheory.Padics.PadicNumbers

Cited by

1 results in Mathlib

Foundations

Depth 87 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fact