instCommRingOfIsAbsoluteValue — Mathlib

English

If β is a commutative ring and abv is an absolute value on β, then CauSeq(β, abv) inherits a commutative ring structure.

Русский

Если β — коммутативное кольцо, и abv — абсолютная величина на β, то CauSeq(β, abv) образует коммутативное кольцо.

LaTeX

$$$CommRing(CauSeq(\beta, abv))$$$

Lean4

instance {β : Type*} [CommRing β] {abv : β → α} [IsAbsoluteValue abv] : CommRing (CauSeq β abv) :=
  { CauSeq.ring with mul_comm := fun a b => ext fun n => by simp [mul_comm] }

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