field — Mathlib

English

The Cauchy completion of a valued field carries a field structure; in particular, CauSeq.Completion.Cauchy abv is a field.

Русский

Завершение по Коши заполнения поля относительно абсолютной величины abv образует поле; CauSeq.Completion.Cauchy abv является полем.

LaTeX

$$$\\mathrm{Field}\\big(\\mathrm{CauSeq.Completion.Cauchy}\\;abv\\big)$$$

Lean4

/-- The Cauchy completion forms a field. -/
noncomputable instance field : Field (Cauchy abv) :=
  { Cauchy.divisionRing, Cauchy.commRing with }

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