no goals
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
⊢ x ^ n = x ^ (n % orderOf x + orderOf x * (n / orderOf x))
rw [Nat.mod_add_div]
no goals
G : Type u
A : Type v
x y : G
a b : A
n✝ m : ℕ
inst✝¹ : Monoid G
inst✝ : AddMonoid A
n : ℕ
⊢ x ^ (n % orderOf x + orderOf x * (n / orderOf x)) = x ^ (n % orderOf x)
simp [pow_add, pow_mul, pow_orderOf_eq_one]