PadicComplex — Mathlib

English

The p-adic complex numbers ℂ_p are defined as the completion of PadicAlgCl(p) with respect to the p-adic norm.

Русский

p-адические комплексные числа ℂ_p определяются как дополнение PadicAlgCl(p) по p-адовой норме.

LaTeX

$$$\mathbb{C}_p = \operatorname{Completion}(\mathrm{PadicAlgCl}(p)).$$$

Lean4

/-- `ℂ_[p]` is the field of `p`-adic complex numbers, that is, the completion of `PadicAlgCl p` with
respect to the `p`-adic norm. -/
abbrev PadicComplex :=
  UniformSpace.Completion (PadicAlgCl p)

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