Wieferich primes

DefinitionWieferich primes#✓fully proved

A natural number \(p\) is a Wieferich prime (to base \(2\)) if \(p\) is prime and \(p^2\) divides \(2^{p-1} - 1\).

def IsWieferichPrime (p : ℕ) : Prop :=
  p.Prime ∧ p ^ 2 ∣ 2 ^ (p - 1) - 1

Used by 5

Used bySquared prime factors of Fermat numbers via Wieferich primes and orders · Wieferich primes via remainders · Wieferich primes via congruences · Regular and non-Wieferich primes give non-vanishing finite multiple zeta values · Wieferich's criterion for the first case of Fermat's Last Theorem

TheoremWieferich primes via congruences#✓fully proved

For every natural number \(p\), \(p\) is a Wieferich prime if and only if \(p\) is prime and \(2^{p-1} \equiv 1 \pmod{p^2}\).

theorem isWieferichPrime_iff_modEq (p : ℕ) :
    p.IsWieferichPrime ↔ p.Prime ∧ 2 ^ (p - 1) ≡ 1 [MOD p ^ 2]

Uses 1 · Used by 2

Statement usesWieferich primes

Used bySquared prime factors of Fermat numbers via Wieferich primes and orders · Wieferich primes via remainders

TheoremWieferich primes via remainders#✓fully proved

For every natural number \(p\), \(p\) is a Wieferich prime if and only if \(p\) is prime and the remainder of \(2^{p-1}\) on division by \(p^2\) is \(1\).

theorem isWieferichPrime_iff_mod (p : ℕ) :
    p.IsWieferichPrime ↔ p.Prime ∧ 2 ^ (p - 1) % (p ^ 2) = 1

Uses 2

Statement usesWieferich primes

Proof usesWieferich primes via congruences

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.