toSemiring

Mathlib.Algebra.Ring.Subsemiring.Defs

URI: https://scilib.ai/kg/mathlib#Subsemiring.toSemiring

← MathLib Explorer

English

A subsemiring of a Semiring R is itself a Semiring.

Русский

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

LaTeX

$$$\text{If } R \text{ is a Semiring and } s \le R, \text{ then } s \text{ is a Semiring}$$$

Lean4

/-- A subsemiring of a `Semiring` is a `Semiring`. -/
instance toSemiring {R} [Semiring R] (s : Subsemiring R) : Semiring s :=
  { s.toNonAssocSemiring, s.toSubmonoid.toMonoid with }

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

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

Разделы

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

Аффилиация

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