instIsStrictOrderedModule

Mathlib.Algebra.Order.Module.Defs

URI: https://scilib.ai/kg/mathlib#OrderDual.instIsStrictOrderedModule

English

A second variant of dual IsStrictOrderedModule.

Русский

Вторая вариация двойственной IsStrictOrderedModule.

LaTeX

$$$[IsStrictOrderedModule α β] \\Rightarrow [IsStrictOrderedModule α β^{\\mathrm{op}}]$$$

Lean4

instance instIsStrictOrderedModule [IsStrictOrderedModule α β] : IsStrictOrderedModule α βᵒᵈ where

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

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

Разделы

Аффилиация

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