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. Mathlib version used by the checker is v4.29.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

Submit Solution

Login to submit a solution.

Recent Submissions