directSumGCommSemiring — Mathlib

English

A direct sum of copies of a Commutative Semiring inherits a commutative semiring structure.

Русский

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

LaTeX

$$$$\text{If }A_i\text{ are copies of a }\text{CommSemiring},\\ \bigoplus_i A_i\text{ inherits a }\text{CommSemiring}.$$$$

Lean4

/-- A direct sum of copies of a `CommSemiring` inherits the commutative multiplication structure. -/
instance directSumGCommSemiring {R : Type*} [AddCommMonoid ι] [CommSemiring R] : DirectSum.GCommSemiring fun _ : ι => R
    where
  __ := Semiring.directSumGSemiring ι
  __ := CommMonoid.gCommMonoid ι

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