no goals
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℤ
⊢ x ^ i = ?m.909316
rw [← Int.emod_add_ediv i (orderOf x)]
no goals
G : Type u
A : Type v
x y : G
a b : A
n m : ℕ
inst✝¹ : Group G
inst✝ : AddGroup A
i : ℤ
⊢ x ^ (i % ↑(orderOf x) + ↑(orderOf x) * (i / ↑(orderOf x))) = x ^ (i % ↑(orderOf x))
simp [zpow_add, zpow_mul, pow_orderOf_eq_one]