directSumGCommRing — Mathlib

English

A direct sum of copies of a Commutative Ring inherits a commutative ring structure.

Русский

Прямая сумма копий коммутативного кольца наследует коммутативное кольцо.

LaTeX

$$$$\text{If }R\text{ is a }\text{CommRing},\\ \bigoplus_i R\text{ is a }\text{CommRing}.$$$$

Lean4

/-- A direct sum of copies of a `CommRing` inherits the commutative multiplication structure. -/
instance directSumGCommRing {R : Type*} [AddCommMonoid ι] [CommRing R] : DirectSum.GCommRing fun _ : ι => R
    where
  __ := Ring.directSumGRing ι
  __ := CommMonoid.gCommMonoid ι

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