normedField — Mathlib

English

For x ∈ ℚ_p, the norm of x considered in PadicAlgCl p equals its p-adic norm in ℚ_p.

Русский

Для x ∈ ℚ_p норма x в PadicAlgCl p совпадает с p-адической нормой в ℚ_p.

LaTeX

$$$$\|x\|_{\operatorname{PadicAlgCl}(p)} = \|x\|_p \quad( x\in \mathbb{Q}_p ).$$$$

Lean4

/-- `PadicAlgCl p` is a normed field, where the norm is the `p`-adic norm, that is, the
spectral norm induced by the `p`-adic norm on `ℚ_[p]`. -/
instance normedField : NormedField (PadicAlgCl p) :=
  spectralNorm.normedField ℚ_[p] (PadicAlgCl p)

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