orderOf_pow_orderOf_div — Mathlib

English

If ord(x) divides n, then ord(x^k) divides ord(x) for k dividing n.

Русский

Если ord(x) делит n, то ord(x^k) делит ord(x) для k, делящего n.

LaTeX

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

Lean4

@[to_additive]
theorem orderOf_pow_orderOf_div {x : G} {n : ℕ} (hx : orderOf x ≠ 0) (hn : n ∣ orderOf x) :
    orderOf (x ^ (orderOf x / n)) = n :=
  by
  rw [orderOf_pow_of_dvd _ (Nat.div_dvd_of_dvd hn), Nat.div_div_self hn hx]
  rw [← Nat.div_mul_cancel hn] at hx; exact left_ne_zero_of_mul hx

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