le_mul_inv_iff_le — Mathlib

English

Let α be a group with a compatible order. Then for all a, b, c ∈ α, 1 ≤ a b^{-1} iff b ≤ a.

Русский

Пусть α – группа с совместимым порядком. Тогда для любых a, b, c ∈ α, 1 ≤ a b^{-1} эквивалентно b ≤ a.

LaTeX

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

Lean4

@[to_additive]
theorem le_mul_inv_iff_le : 1 ≤ a * b⁻¹ ↔ b ≤ a := by rw [← mul_le_mul_iff_right b, one_mul, inv_mul_cancel_right]

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