instNormedField — Mathlib

English

ℂ_p is a normed field with respect to the extended valuation.

Русский

ℂ_p является нормированным полем относительно расширенной оценки.

LaTeX

$$$\mathbb{C}_p \text{ is a normed field with norm } \|\cdot\| = \mathrm{Norm}.\text{norm}$$$

Lean4

/-- `ℂ_[p]` is a normed field, where the norm corresponds to the extension of the `p`-adic
  valuation. -/
instance : NormedField ℂ_[p] :=
  Valued.toNormedField _ _

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