leOnePart_eq_inv' — Mathlib

English

In a lattice-ordered group, the equality a⁻ᵐ = a⁻¹ holds exactly when 1 ≤ a⁻¹.

Русский

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

LaTeX

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

Lean4

/-- See also `leOnePart_eq_inv`. -/
@[to_additive /-- See also `negPart_eq_neg`. -/
    ]
theorem leOnePart_eq_inv' : a⁻ᵐ = a⁻¹ ↔ 1 ≤ a⁻¹ :=
  sup_eq_left

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