PadicSeq — Mathlib

English

PadicSeq denotes the type of Cauchy sequences of rationals with respect to the p-adic norm.

Русский

PadicSeq обозначает множество Коши-последовательностей рациональных чисел по p-адической норме.

LaTeX

$$\\text{PadicSeq}(p) := \\ CauSeq_{\\mathbb{Q}}(\\|\\cdot\\|_p)$$

Lean4

/-- The type of Cauchy sequences of rationals with respect to the `p`-adic norm. -/
abbrev PadicSeq (p : ℕ) :=
  CauSeq _ (padicNorm p)

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