Fermat quotients

DefinitionFermat quotient#✓fully proved

For a prime \(p\) and an integer \(a\) coprime to \(p\), the Fermat quotient is the integer \(q_p(a) = (a^{p-1} - 1)/p\), where \(/\) is integer division rounding down. The division is exact, since \(p\) divides \(a^{p-1} - 1\) by Fermat's little theorem.

@[nolint unusedArguments]
def fermatQuotient (p : ℕ) (_hp : Nat.Prime p) (a : ℤ)
    (_ha : IsCoprime a (p : ℤ)) : ℤ :=
  (a ^ (p - 1) - 1) / (p : ℤ)

Used by 7

Used byDelannoy triangle entry \(T(np-1, p-1; 1)\) modulo \(p^3\) · Delannoy triangle entries \(T(2p, p; 1)\) and \(T(2p-1, p-1; 1)\) modulo \(p^3\) · Sum of \(H_k 2^k / k\) over \(1 \le k \le p - 1\) modulo \(p\) · Sums of \(2^k/k\) and \(2^k/k^2\) over \(1 \le k \le p - 1\) · Formula for the Fermat quotient · Fermat quotient times the prime · Wilson's theorem modulo \(p^2\)

TheoremFormula for the Fermat quotient#✓fully proved

For a prime \(p\) and an integer \(a\) coprime to \(p\), the Fermat quotient satisfies \(q_p(a) = (a^{p-1} - 1)/p\), where \(/\) is integer division rounding down.

theorem fermatQuotient_eq (p : ℕ) (hp : Nat.Prime p) (a : ℤ)
    (ha : IsCoprime a (p : ℤ)) :
    fermatQuotient p hp a ha = (a ^ (p - 1) - 1) / (p : ℤ)

Uses 1

Statement usesFermat quotient

TheoremFermat quotient times the prime#✓fully proved

For a prime \(p\) and an integer \(a\) coprime to \(p\), the Fermat quotient \(q_p(a)\) satisfies \(p \, q_p(a) = a^{p-1} - 1\).

theorem natCast_mul_fermatQuotient (p : ℕ) (hp : Nat.Prime p) (a : ℤ)
    (ha : IsCoprime a (p : ℤ)) :
    (p : ℤ) * fermatQuotient p hp a ha = a ^ (p - 1) - 1

Uses 1

Statement usesFermat quotient

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.