zpow — Mathlib

English

From a finite order element, all its integer powers have finite order.

Русский

Из элемента конечного порядка все его целочисленные степени также имеют конечный порядок.

LaTeX

$$∀ h: IsOfFinOrder x, ∀ i ∈ ℤ, IsOfFinOrder (x^i)$$

Lean4

@[to_additive]
theorem zpow (h : IsOfFinOrder x) {i : ℤ} : IsOfFinOrder (x ^ i) :=
  isOfFinOrder_iff_pow_eq_one.mpr ⟨orderOf x, h.orderOf_pos, zpow_pow_orderOf⟩

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