div_lt_comm

Mathlib.Algebra.Order.Group.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#div_lt_comm

English

In a commutative group with order, a/b < c ↔ a/c < b.

Русский

В коммутативной группе с порядком, a/b < c ⇔ a/c < b.

LaTeX

$$$\dfrac{a}{b} < c \iff \dfrac{a}{c} < b$$$

Lean4

@[to_additive]
theorem div_lt_comm : a / b < c ↔ a / c < b :=
  div_lt_iff_lt_mul'.trans div_lt_iff_lt_mul.symm

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

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

Разделы

Аффилиация

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