instSemiring

Mathlib.Algebra.Ring.Prod

URI: https://scilib.ai/kg/mathlib#Prod.instSemiring

← MathLib Explorer

English

Product of two semirings is a semiring.

Русский

Произведение двух полукольц является полукольцом.

LaTeX

$$$\text{Semiring}(R \times S)$$$

Lean4

/-- Product of two semirings is a semiring. -/
instance instSemiring [Semiring R] [Semiring S] : Semiring (R × S) :=
  { inferInstanceAs (NonUnitalSemiring (R × S)), inferInstanceAs (NonAssocSemiring (R × S)),
    inferInstanceAs (MonoidWithZero (R × S)) with }

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

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

Разделы

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

Аффилиация

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