English
If n is coprime to ord(x), there exists m with (x^n)^m = x.
Русский
Если n взаимно простое с ord(x), существует m такое, что (x^n)^m = x.
LaTeX
$$$ \forall G [Monoid G], \forall x : G, \forall n : \mathbb{N}, \; \gcd(n, ord(x)) = 1 \Rightarrow \exists m : \mathbb{N}, (x^n)^m = x$$$
Lean4
@[to_additive]
theorem exists_pow_eq_self_of_coprime (h : n.Coprime (orderOf x)) : ∃ m : ℕ, (x ^ n) ^ m = x :=
by
by_cases h0 : orderOf x = 0
· rw [h0, coprime_zero_right] at h
exact ⟨1, by rw [h, pow_one, pow_one]⟩
by_cases h1 : orderOf x = 1
· exact ⟨0, by rw [orderOf_eq_one_iff.mp h1, one_pow, one_pow]⟩
obtain ⟨m, h⟩ := exists_mul_emod_eq_one_of_coprime h (one_lt_iff_ne_zero_and_ne_one.mpr ⟨h0, h1⟩)
exact ⟨m, by rw [← pow_mul, ← pow_mod_orderOf, h, pow_one]⟩
