PowGCD

Let $a, n$ be integers and $n > 0$. Prove that $n$ divides $\sum_{k=1}^{n} a^{\gcd(k, n)}$.

Replace sorry in the template below with your solution. The Mathlib version currently used is v4.26.0.

import Mathlib.Order.Interval.Finset.Nat
import Mathlib.Data.Fintype.BigOperators

theorem solution {a : ℤ} {n : ℕ} (hn : n > 0) :
    (n : ℤ) ∣ ∑ k ∈ (Finset.Icc 1 n), a ^ (k.gcd n) := sorry

Login to submit a solution.