isOfFinOrder_iff_pow_eq_one — Mathlib

English

In a division monoid, IsOfFinOrder x is equivalent to the existence of a nonzero integer n with x^n = 1.

Русский

В делимом моноиде IsOfFinOrder x эквивалентно существованию ненулевого целого n с x^n = 1.

LaTeX

$$$IsOfFinOrder(x) \iff \exists n \in \mathbb{Z}, n \neq 0 \wedge x^n = 1$$$

Lean4

@[to_additive]
theorem isOfFinOrder_iff_pow_eq_one : IsOfFinOrder x ↔ ∃ n, 0 < n ∧ x ^ n = 1 := by
  simp [IsOfFinOrder, mem_periodicPts, isPeriodicPt_mul_iff_pow_eq_one]

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