Cauchy

Mathlib.Algebra.Order.CauSeq.Completion

URI: https://scilib.ai/kg/mathlib#CauSeq.Completion.Cauchy

English

The Cauchy completion is the quotient of CauSeq by the equivalence relation.

Русский

Замыкание по Коши является фактор-гранью CauSeq по эквивалентности.

LaTeX

$$$\mathrm{CauSeq.Completion.Cauchy} = \mathrm{Quotient}(\mathrm{CauSeq}(\alpha, \mathrm{abs}), \sim)$$$

Lean4

/-- The Cauchy completion of a ring with absolute value. -/
def Cauchy :=
  @Quotient (CauSeq _ abv) CauSeq.equiv

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru