Congruences and modular arithmetic
Congruences for factorials, quotients and power sums (Wilson, Wolstenholme, Fermat quotients), lifting the exponent, multiplicative order, primitive roots, residue systems.
- Arithmetic progressions in reduced residue systems
- Euler–Fermat congruences modulo prime powers
- Fermat quotients
- Congruences for Delannoy numbers
- Lifting the exponent lemma
- Modular inverses from the Euclidean algorithm
- Primitive roots modulo prime powers
- Primitive λ-roots
- Small solutions of diagonal congruences
- Thue's lemma
- Wilson quotients
- Wolstenholme's theorem
TheoremPower sums vanish modulo a prime#✓fully proved
MetaMathlibExt.powerSum_vanishing_mod_prime
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
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
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.