English
The Cauchy completion with respect to abv carries a ring structure, i.e., both addition and multiplication are defined and satisfy ring axioms inside CauSeq.Completion.Cauchy abv.
Русский
У дополнения Коши относительно abv есть структура кольца: сложение и умножение определены и удовлетворяют axioms кольца в CauSeq.Completion.Cauchy abv.
LaTeX
$$$\text{CauSeq.Completion.Cauchy abv is a ring}$$$
Lean4
instance ring : Ring (Cauchy abv) :=
fast_instance%Function.Surjective.ring mk Quotient.mk'_surjective zero_def.symm one_def.symm
(fun _ _ => (mk_add _ _).symm) (fun _ _ => (mk_mul _ _).symm) (fun _ => (mk_neg _).symm)
(fun _ _ => (mk_sub _ _).symm) (fun _ _ => (mk_smul _ _).symm) (fun _ _ => (mk_smul _ _).symm)
(fun _ _ => (mk_pow _ _).symm) (fun _ => rfl) fun _ => rfl
