instIsOrderedModule

Mathlib.Algebra.Order.Module.Defs

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

English

Alternative dual instantiation for IsOrderedModule.

Русский

Альтернативная двойственная реализация IsOrderedModule.

LaTeX

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

Lean4

instance instIsOrderedModule [IsOrderedModule α β] : IsOrderedModule α βᵒᵈ where

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

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

Разделы

Аффилиация

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