directSumGNonUnitalNonAssocSemiring

Mathlib.Algebra.DirectSum.Ring

URI: https://scilib.ai/kg/mathlib#NonUnitalNonAssocSemiring.directSumGNonUnitalNonAssocSemiring

Lean4

/-- A direct sum of copies of a `NonUnitalNonAssocSemiring` inherits the multiplication structure.
-/
instance directSumGNonUnitalNonAssocSemiring {R : Type*} [AddMonoid ι] [NonUnitalNonAssocSemiring R] :
    DirectSum.GNonUnitalNonAssocSemiring fun _ : ι => R :=
  { -- Porting note: removed Mul.gMul ι with and we seem ok

    mul_zero := mul_zero
    zero_mul := zero_mul
    mul_add := mul_add
    add_mul := add_mul }

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru