orderOf_pow_of_dvd — Mathlib

English

For any x and n, if ord(x) ≠ 0 and n ∣ ord(x), then ord(x^{ord(x)/n}) = ord(x)/n.

Русский

Для любого x и n, если ord(x) ≠ 0 и n делит ord(x), то ord(x^{ord(x)/n}) = ord(x)/n.

LaTeX

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

Lean4

@[to_additive]
theorem orderOf_pow_of_dvd {x : G} {n : ℕ} (hn : n ≠ 0) (dvd : n ∣ orderOf x) : orderOf (x ^ n) = orderOf x / n := by
  rw [orderOf_pow' _ hn, Nat.gcd_eq_right dvd]

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