Congruences and modular arithmetic

Congruences for factorials, quotients and power sums (Wilson, Wolstenholme, Fermat quotients), lifting the exponent, multiplicative order, primitive roots, residue systems.

TheoremPower sums vanish modulo a prime#✓fully proved

Let \(p\) be a prime and let \(e \ge 0\) be an integer such that \(p - 1\) does not divide \(e\) whenever \(e \ge 1\). Then \(p\) divides \(\sum_{t=1}^{p} t^e\).

For \(e = 0\) the sum is \(p\). The source states the lemma for odd primes; for \(p = 2\) the hypothesis forces \(e = 0\).

theorem powerSum_vanishing_mod_prime
    (p : ℕ) (hp : Nat.Prime p) (e : ℕ)
    (he : 1 ≤ e → ¬ (p - 1) ∣ e) :
    (p : ℤ) ∣ ∑ t ∈ Finset.Icc 1 p, (t : ℤ) ^ e
Sources
  • Christian Ballot, "On a Congruence of Kimball and Webb Involving Lucas Sequences," Journal of Integer Sequences 17 (2014), Article 14.1.3, Lemma, lines 223–225, https://cs.uwaterloo.ca/journals/JIS/VOL17/Ballot/ballot7.tex

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.