English
There is a ring isomorphism between the real numbers and the Cauchy completion of the rationals with respect to the absolute value, given by toFun = cauchy and invFun = ofCauchy, preserving addition and multiplication.
Русский
Существует кольцевое изоморфизм между действительными числами и Каноническим завершением по Коши рациональных чисел относительно модуля абсолютной величины, заданный отображениями toFun = cauchy и invFun = ofCauchy, сохраняющий сложение и умножение.
LaTeX
$$$\mathbb{R} \cong_{\text{ring}} \mathrm{CauSeq.Completion.Cauchy}(|\cdot|)$$$
Lean4
/-- `Real.equivCauchy` as a ring equivalence. -/
@[simps]
def ringEquivCauchy : ℝ ≃+* CauSeq.Completion.Cauchy (abs : ℚ → ℚ) :=
{ equivCauchy with
toFun := cauchy
invFun := ofCauchy
map_add' := cauchy_add
map_mul' := cauchy_mul }
