orderOf_pow' — Mathlib

English

If ord(x) ≠ 0 and n divides ord(x), then ord(x^{ord(x)/n}) = n.

Русский

Если ord(x) ≠ 0 и n делит ord(x), то ord(x^{ord(x)/n}) = n.

LaTeX

$$$ \forall {G} [Monoid G] {x : G} {n : \mathbb{N}}, ord(x) \neq 0 ∧ n \mid ord(x) \rightarrow ord(x^{ord(x)/n}) = n$$$

Lean4

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

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