toIsStrictOrderedRing

Mathlib.Algebra.Ring.Subsemiring.Order

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

← MathLib Explorer

English

IsStrictOrderedRing holds for a subsemiring.

Русский

IsStrictOrderedRing выполняется для подпол semiring.

LaTeX

$$$\\text{IsStrictOrderedRing}(S)$$$

Lean4

/-- A subsemiring of a strict ordered semiring is a strict ordered semiring. -/
instance toIsStrictOrderedRing [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] (s : Subsemiring R) :
    IsStrictOrderedRing s :=
  SubsemiringClass.toIsStrictOrderedRing _

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

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

Разделы

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

Аффилиация

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