no goals
G : Type u
inst✝ : Monoid G
n : ℕ
g : G
⊢ g ^ n = g ^ (n % exponent G + exponent G * (n / exponent G))
rw [Nat.mod_add_div]
no goals
G : Type u
inst✝ : Monoid G
n : ℕ
g : G
⊢ g ^ (n % exponent G + exponent G * (n / exponent G)) = g ^ (n % exponent G)
simp [pow_add, pow_mul, pow_exponent_eq_one]