orderedSubtype_coe

Mathlib.Algebra.Ring.Subring.Order

URI: https://scilib.ai/kg/mathlib#Subring.orderedSubtype_coe

English

The two order-preserving inclusions coincide: orderedSubtype s = subtype s.

Русский

Два порядка сохраняющих включения совпадают: orderedSubtype s = subtype s.

LaTeX

$$$\text{orderedSubtype}(s) = \text{subtype}(s)$$$

Lean4

theorem orderedSubtype_coe (s : Subring R) : Subring.orderedSubtype s = Subring.subtype s :=
  rfl

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

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

Разделы

Аффилиация

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