one_lt_inv_iff — Mathlib

English

Under a right-monotone order in a group, 1 < a^{-1} iff a < 1.

Русский

При правой монотонности порядка в группе, 1 < a^{-1} тогда же, что и a < 1.

LaTeX

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

Lean4

/-- Uses `right` co(ntra)variant. -/
@[to_additive (attr := simp) Right.neg_pos_iff /-- Uses `right` co(ntra)variant. -/
    ]
theorem one_lt_inv_iff : 1 < a⁻¹ ↔ a < 1 := by rw [← mul_lt_mul_iff_right a, inv_mul_cancel, one_mul]

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