inv_mul_lt_iff_lt_mul

Mathlib.Algebra.Order.Group.Unbundled.Basic

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

English

In a group with order and left-mono, b⁻¹ a < c iff a < b c.

Русский

В группе с порядком и левым монотонным умножением: b⁻¹ a < c тогда, когда a < b c.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem inv_mul_lt_iff_lt_mul : b⁻¹ * a < c ↔ a < b * c := by rw [← mul_lt_mul_iff_left b, mul_inv_cancel_left]

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

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

Разделы

Аффилиация

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