leOnePart_eq_one' — Mathlib

English

In a lattice-ordered group, the statement a⁻ᵐ = a⁻¹ is equivalent to 1 ≤ a⁻¹.

Русский

Для элемента a в решёточно упорядоченной группе равенство a⁻ᵐ = a⁻¹ эквивалентно 1 ≤ a⁻¹.

LaTeX

$$$a^{-m} = a^{-1} \iff 1 \le a^{-1}$$$

Lean4

/-- See also `leOnePart_eq_one`. -/
@[to_additive /-- See also `negPart_eq_zero`. -/
    ]
theorem leOnePart_eq_one' : a⁻ᵐ = 1 ↔ a⁻¹ ≤ 1 :=
  sup_eq_right

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