orderOf_pow — Mathlib

English

If ord(y) is coprime to m, then ord(y^m) = ord(y).

Русский

Если ord(y) взаимно прост с m, тогда ord(y^m) = ord(y).

LaTeX

$$$ \forall {G} [Monoid G] {y : G} {m : \mathbb{N}}, (ord(y)).Coprime m → ord(y^m) = ord(y)$$$

Lean4

@[to_additive]
theorem orderOf_pow (h : (orderOf y).Coprime m) : orderOf (y ^ m) = orderOf y :=
  by
  by_cases hg : IsOfFinOrder y
  · rw [hg.orderOf_pow y m, h.gcd_eq_one, Nat.div_one]
  · rw [m.coprime_zero_left.1 (orderOf_eq_zero hg ▸ h), pow_one]

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