normedField — Mathlib

English

If K is a field and v is a real-valued absolute value on K, then the construction WithAbs v carries a NormedField structure; i.e., WithAbs v is a normed field.

Русский

Если K — поле и v — действительное абсолютное значение на K, то конструкция WithAbs v наделяет WithAbs v структурой нормированного поля, то есть WithAbs v является нормированным полем.

LaTeX

$$$$\\text{NormedField}(\\mathrm{WithAbs}(v)).$$$$

Lean4

instance normedField [Field R] (v : AbsoluteValue R ℝ) : NormedField (WithAbs v) :=
  v.toNormedField

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