lt_mul_inv_iff_lt

Mathlib.Algebra.Order.Group.Unbundled.Basic

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

English

In a linearly ordered group with a left-monotone multiplication, 1 < a b^{-1} if and only if b < a.

Русский

В линейно упорядоченной группе с левым монотонным умножением выполняется 1 < a b^{-1} ↔ b < a.

LaTeX

$$$1 < a \cdot b^{-1} \iff b < a$$$

Lean4

@[to_additive]
theorem lt_mul_inv_iff_lt : 1 < a * b⁻¹ ↔ b < a := by rw [← mul_lt_mul_iff_right b, one_mul, inv_mul_cancel_right]

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

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

Разделы

Аффилиация

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