orderOf_pow — Mathlib

English

If x has finite order, then ord(x^n) = ord(x)/gcd(ord(x), n).

Русский

Если ord(x) конечен, то ord(x^n) = ord(x) / gcd(ord(x), n).

LaTeX

$$$ \forall {G} [Monoid G] {x : G} {n : \mathbb{N}}, IsOfFinOrder x → ord(x^n) = ord(x) / gcd(ord(x), n)$$$

Lean4

@[to_additive]
protected theorem orderOf_pow (h : IsOfFinOrder x) : orderOf (x ^ n) = orderOf x / gcd (orderOf x) n :=
  by
  unfold orderOf
  rw [← minimalPeriod_iterate_eq_div_gcd' h, mul_left_iterate]

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