isOfFinOrder_inv_iff — Mathlib

English

In any group, an element x has finite order if and only if its inverse x^{-1} has finite order.

Русский

В группе элемент x имеет конечный порядок тогда и только тогда, когда обратный элемент x^{-1} имеет конечный порядок.

LaTeX

$$$\\IsOfFinOrder\\ x^{-1} \\Leftrightarrow \\IsOfFinOrder\\ x$$$

Lean4

/-- Inverses of elements of finite order have finite order. -/
@[to_additive (attr := simp) /-- Inverses of elements of finite additive order
    have finite additive order. -/
    ]
theorem isOfFinOrder_inv_iff {x : G} : IsOfFinOrder x⁻¹ ↔ IsOfFinOrder x := by simp [isOfFinOrder_iff_pow_eq_one]

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