Theorem: Group.pow_eq_zpow_mod (AntLorentz/CyclotomicCharacter.lean)

State before:
L : Type u
inst✝¹ : Field L
n✝ : ℕ+
G : Type u_1
inst✝ : Group G
x : G
m : ℤ
n : ℕ
h : x ^ n = 1
⊢ x ^ m = x ^ (m % ↑n)
Tactic:
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
State after:
L : Type u
inst✝¹ : Field L
n✝ : ℕ+
G : Type u_1
inst✝ : Group G
x : G
m : ℤ
n : ℕ
h : x ^ n = 1
h2 : x ^ m = x ^ (↑n * (m / ↑n) + m % ↑n)
⊢ x ^ m = x ^ (m % ↑n)

State before:
L : Type u
inst✝¹ : Field L
n✝ : ℕ+
G : Type u_1
inst✝ : Group G
x : G
m : ℤ
n : ℕ
h : x ^ n = 1
h2 : x ^ m = x ^ (↑n * (m / ↑n) + m % ↑n)
⊢ x ^ m = x ^ (m % ↑n)
Tactic:
simp [h, h2, zpow_add, zpow_mul]
State after:
no goals