Euler–Fermat congruences modulo prime powers

TheoremEuler–Fermat congruence modulo prime powers#✓fully proved

For every natural number \(a\), every prime \(p\) and every natural number \(r \ge 1\), we have \(a^{p^r} \equiv a^{p^{r-1}} \pmod{p^r}\).

theorem euler_fermat_prime_power_congruence_general {a p r : ℕ} (hp : Nat.Prime p)
    (hr : 1 ≤ r) : Nat.ModEq (p ^ r) (a ^ (p ^ r)) (a ^ (p ^ (r - 1)))

Used by 1

Used byEuler–Fermat congruence modulo prime powers, for positive bases

TheoremEuler–Fermat congruence modulo prime powers, for positive bases#✓fully proved

For every positive natural number \(a\), every prime \(p\) and every natural number \(r \ge 1\), we have \(a^{p^r} \equiv a^{p^{r-1}} \pmod{p^r}\).

theorem euler_fermat_prime_power_congruence {a p r : ℕ}
    (ha : 0 < a) (hp : Nat.Prime p) (hr : 1 ≤ r) :
    Nat.ModEq (p ^ r) (a ^ (p ^ r)) (a ^ (p ^ (r - 1)))

Sources

• G. Everest, A. J. van der Poorten, Y. Puri, and T. Ward, "Integer Sequences and Periodic Points," Journal of Integer Sequences 5 (2002), Article 02.2.3, Corollary; public TeX: https://cs.uwaterloo.ca/journals/JIS/VOL5/Ward/ward2.tex. It follows from euler_fermat_prime_power_congruence_general; the hypothesis ha is unused and keeps the source's shape.

Uses 1

Proof usesEuler–Fermat congruence modulo prime powers

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.