mul_inv_lt_iff_lt_mul — Mathlib

English

For a, b, c in a group with right monotone order, a b^{-1} < c implies a < c b, and conversely.

Русский

Для a, b, c в группе с правой монотонностью порядка, a b^{-1} < c тогда и только тогда, когда a < c b.

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem mul_inv_lt_iff_lt_mul : a * b⁻¹ < c ↔ a < c * b := by rw [← mul_lt_mul_iff_right b, inv_mul_cancel_right]

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