toIsStrictOrderedModule

Mathlib.Algebra.Order.Module.Defs

URI: https://scilib.ai/kg/mathlib#IsStrictOrderedRing.toIsStrictOrderedModule

English

For hb > 0, a1 • b < a2 • b ↔ a1 < a2.

Русский

Для hb > 0: a1 • b < a2 • b ⇔ a1 < a2.

LaTeX

$$$hb > 0 \Rightarrow (a_1 \cdot b < a_2 \cdot b \iff a_1 < a_2)$$$

Lean4

instance (priority := 100) toIsStrictOrderedModule [IsStrictOrderedRing α] : IsStrictOrderedModule α α where

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

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

Разделы

Аффилиация

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