pow_eq_zpow_mod

Stream: Is there code for X?

[Kevin Buzzard]

Do we have this?

import Mathlib.Tactic

theorem Group.pow_eq_zpow_mod {G : Type _} [Group G] {x : G} (m : ℤ) {n : ℕ} (h : x ^ n = 1) :
    x ^ m = x ^ (m % (n : ℤ)) := by
  have h2 : x ^ m = x ^ ((n : ℤ) * (m / (n : ℤ)) + m % (n : ℤ)) :=
    congr_arg (fun a => x ^ a) ((Int.add_comm _ _).trans (Int.emod_add_ediv _ _)).symm
  simp [h, h2, zpow_add, zpow_mul]

I found it useful recently. Or should I be using something else? If we want it, does it go in Algebra.GroupPower.Lemmas?

[Scott Morrison]

Sounds good.

#find_home Group.pow_eq_zpow_mod     -- Mathlib.Algebra.GroupPower.Lemmas

[Eric Wieser]

Another option would presumably be to go via docs#orderOf and show it divides n?

[Yaël Dillies]

Why not make n an integer? And if you want to have a look I have similar lemmas here.