commRing — Mathlib

English

The Cauchy completion with abv admits a commutative ring structure, so addition and multiplication commute and satisfy ring axioms.

Русский

Дополнение Коши с abv образует коммутативное кольцо: сложение и умножение коммутируют и удовлетворяют аксиомам кольца.

LaTeX

$$$\text{CauSeq.Completion.Cauchy abv}$ is a commutative ring.$$

Lean4

instance commRing : CommRing (Cauchy abv) :=
  fast_instance%Function.Surjective.commRing 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

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