toIsOrderedModule

Mathlib.Algebra.Order.Module.Defs

URI: https://scilib.ai/kg/mathlib#IsOrderedRing.toIsOrderedModule

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 \le a_2 \cdot b \iff a_1 \le a_2)$$$

Lean4

instance (priority := 100) toIsOrderedModule [IsOrderedRing α] : IsOrderedModule α α where
  -- See note [lower instance priority]

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

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

Разделы

Аффилиация

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