zpow_pow_orderOf — Mathlib

English

If x has finite order, then x^i has finite order for every integer i.

Русский

Если у x конечный порядок, то x^i имеет конечный порядок при любом целочисленном i.

LaTeX

$$IsOfFinOrder x → ∀ i ∈ ℤ, IsOfFinOrder (x^i)$$

Lean4

@[to_additive (attr := simp) zsmul_smul_addOrderOf]
theorem zpow_pow_orderOf : (x ^ i) ^ orderOf x = 1 :=
  by
  by_cases h : IsOfFinOrder x
  · rw [← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast, pow_orderOf_eq_one, one_zpow]
  · rw [orderOf_eq_zero h, _root_.pow_zero]

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