inv_le_one_iff — Mathlib

English

In a group with a compatible order and left-monotone multiplication, a⁻¹ ≤ 1 holds if and only if 1 ≤ a.

Русский

В группе с упорядочением и левой мономотой умножения неравенство a⁻¹ ≤ 1 эквивалентно 1 ≤ a.

LaTeX

$$$a^{-1} \le 1 \ \Leftrightarrow \ 1 \le a$$$

Lean4

/-- Uses `left` co(ntra)variant. -/
@[to_additive (attr := simp) /-- Uses `left` co(ntra)variant. -/
    ]
theorem inv_le_one_iff : a⁻¹ ≤ 1 ↔ 1 ≤ a := by
  rw [← mul_le_mul_iff_left a]
  simp

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