Wilson quotients

DefinitionWilson quotient#✓fully proved

For a natural number \(p\), the Wilson quotient is the integer \(W(p) = \lfloor ((p-1)! + 1) / p \rfloor\) for \(p \ge 1\), and \(W(0) = 0\).

For a prime \(p\), Wilson's theorem \(p \mid (p-1)! + 1\) makes the division exact. The definition is total on \(\mathbb{N}\); the source defines \(W_p\) only for odd primes \(p\).

def wilsonQuotient (p : ℕ) : ℤ :=
  ((Nat.factorial (p - 1) : ℤ) + 1) / (p : ℤ)

Sources

Y. Matsuno, A resolution of Kellner's conjectures on Wilson quotients, arXiv:2607.10106v1, lines 44–51.

Used by 2

Used byFactorial form of the Wilson quotient identity · Exactness of the Wilson quotient

TheoremExactness of the Wilson quotient#✓fully proved

For every prime \(p\), the Wilson quotient \(W(p)\) of \(p\) satisfies \(p \, W(p) = (p-1)! + 1\) in \(\mathbb{Z}\).

By Wilson's theorem \(p\) divides \((p-1)! + 1\), so the division defining \(W(p)\) is exact.

theorem mul_wilsonQuotient (p : ℕ) (hp : Nat.Prime p) :
    (p : ℤ) * wilsonQuotient p = (Nat.factorial (p - 1) : ℤ) + 1

Sources

M. Avitabile and S. Mattarei, arXiv:2308.16034, AH.tex lines 315–321, which uses \((p-1)! = -1 + p \, w_p\), where \(w_p\) is the Wilson quotient.

Uses 1 · Used by 1

Statement usesWilson quotient

Used byFactorial form of the Wilson quotient identity

TheoremFactorial form of the Wilson quotient identity#✓fully proved

For every prime \(p\), the Wilson quotient \(W(p)\) of \(p\) satisfies \((p-1)! = p \, W(p) - 1\) in \(\mathbb{Z}\).

theorem factorial_eq_mul_wilsonQuotient_sub_one (p : ℕ) (hp : Nat.Prime p) :
    (Nat.factorial (p - 1) : ℤ) = (p : ℤ) * wilsonQuotient p - 1

Sources

M. Avitabile and S. Mattarei, arXiv:2308.16034, AH.tex lines 315–321, display \((p-1)! = -1 + p \, w_p\), where \(w_p\) is the Wilson quotient.

Uses 2

Statement usesWilson quotient

Proof usesExactness of the Wilson quotient

TheoremWilson's theorem modulo \(p^2\)#●ready to prove

Let \(p\) be an odd prime and, for \(1 \le k \le p - 1\), let \(q_p(k)\) be the Fermat quotient of \(k\), the integer with \(k^{p-1} = 1 + p\, q_p(k)\). Then

\[ (p - 1)! \equiv -1 + p \sum_{k=1}^{p-1} q_p(k) \pmod{p^2}. \]

theorem_wanted wilson_mod_prime_sq (p : ℕ) (hp : p.Prime)
    (hp2 : p ≠ 2) :
    (Nat.factorial (p - 1) : ZMod (p ^ 2)) =
      -1 + (p : ZMod (p ^ 2)) *
        ∑ k ∈ (Finset.Icc 1 (p - 1)).attach,
          ((Int.fermatQuotient p hp (k.1 : ℤ)
            (coprime_of_mem hp k.2) : ℤ) : ZMod (p ^ 2))

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

MathlibExt/NumberTheory/FermatQuotient.lean:28

private theorem coprime_of_mem {p k : ℕ} (hp : p.Prime)
    (h : k ∈ Finset.Icc 1 (p - 1)) : IsCoprime (k : ℤ) (p : ℤ)

WantedExt/NumberTheory/WilsonFaulhaberWanted.lean:50

Sources

Claire Levaillant, "Wilson's Theorem Modulo p^2 Derived from Faulhaber Polynomials", Theorem 1.

Uses 1

Statement usesFermat quotient

DefinitionMorozov's Wilson quotients#✓fully proved

For natural numbers \(k\) and \(n\), \(M_k(n)\) is the rational number

\[M_k(n) = \frac{1 + (-1)^k \, k! \, (n - k - 1)!}{n},\]

where \(n - k - 1\) is truncated subtraction of natural numbers and division by \(0\) gives \(0\).

def wilsonQuotientM (k n : ℕ) : ℚ :=
  (1 + (-1 : ℚ) ^ k * (Nat.factorial k * Nat.factorial (n - k - 1) : ℚ)) / n

Used by 1

Used byMorozov's Wilson quotient sum

DefinitionMorozov's sign-adjusted Wilson quotients#✓fully proved

For natural numbers \(k\) and \(n\), \(M_k^+(n)\) is the rational number

\[M_k^+(n) = \frac{(-1)^k + k! \, (n - k - 1)!}{n},\]

where \(n - k - 1\) is truncated subtraction of natural numbers and division by \(0\) gives \(0\).

def wilsonQuotientMPlus (k n : ℕ) : ℚ :=
  ((-1 : ℚ) ^ k + (Nat.factorial k * Nat.factorial (n - k - 1) : ℚ)) / n

Used by 1

Used byMorozov's sign-adjusted Wilson quotient sum

DefinitionMorozov's Wilson quotient sum#✓fully proved

For a natural number \(n\), \(Z(n)\) is the rational number \(Z(n) = \sum_{k=0}^{n-1} M_k(n)\), where \(M_k(n)\) are Morozov's Wilson quotients.

def wilsonQuotientZ (n : ℕ) : ℚ :=
  ∑ k ∈ Finset.range n, wilsonQuotientM k n

Uses 1 · Used by 3

Statement usesMorozov's Wilson quotients

Used byThe Wilson quotient sum is an integer · The Wilson quotient sum Z(n) modulo n · A primality criterion from the Wilson quotient sum Z(2n − 1)

DefinitionMorozov's sign-adjusted Wilson quotient sum#✓fully proved

For a natural number \(n\), \(Z^+(n)\) is the rational number \(\sum_{k=0}^{n-1} M_k^+(n)\), where \(M_k^+(n) = ((-1)^k + k!\,(n-k-1)!)/n\) is Morozov's sign-adjusted quotient.

def wilsonQuotientZPlus (n : ℕ) : ℚ :=
  ∑ k ∈ Finset.range n, wilsonQuotientMPlus k n

Uses 1 · Used by 3

Statement usesMorozov's sign-adjusted Wilson quotients

Used byThe sign-adjusted Wilson quotient sum Z⁺(2n) modulo 2n · When the sign-adjusted Wilson quotient sum is a natural number · A Bernoulli–harmonic congruence for the sign-adjusted Wilson quotient sum

TheoremA generalized Wilson criterion for primality#●ready to prove

Let \(n \ge 1\) and \(k < n\) be natural numbers. Then \((-1)^k \, k! \, (n - k - 1)! \equiv -1 \pmod{n}\) if and only if \(n = 1\) or \(n\) is prime.

theorem_wanted neg_one_pow_mul_factorial_mul_factorial_modEq_neg_one_iff
    (n k : ℕ) (hn : 1 ≤ n) (hk : k < n) :
    ((-1 : ℤ) ^ k * (Nat.factorial k * Nat.factorial (n - k - 1) : ℤ) ≡
        -1 [ZMOD (n : ℤ)]) ↔
      n = 1 ∨ n.Prime

Sources

Ivan V. Morozov, "On Quotients of a More General Theorem of Wilson", Corollary 1.

TheoremThe Wilson quotient sum is an integer#●ready to prove

For every natural number \(n \ge 1\), Morozov's Wilson quotient sum \(Z(n)\) is an integer.

theorem_wanted exists_int_eq_wilsonQuotientZ
    (n : ℕ) (hn : 1 ≤ n) :
    ∃ z : ℤ, (z : ℚ) = wilsonQuotientZ n

Sources

Ivan V. Morozov, "On Quotients of a More General Theorem of Wilson", Theorem 1.

Uses 1

Statement usesMorozov's Wilson quotient sum

TheoremWhen the sign-adjusted Wilson quotient sum is a natural number#●ready to prove

For every natural number \(n \ge 1\), Morozov's sign-adjusted Wilson quotient sum \(Z^+(n)\) is a natural number if and only if \(n\) is even, \(n = 1\), or \(n\) is prime.

theorem_wanted exists_nat_eq_wilsonQuotientZPlus_iff
    (n : ℕ) (hn : 1 ≤ n) :
    (∃ m : ℕ, (m : ℚ) = wilsonQuotientZPlus n) ↔
      n % 2 = 0 ∨ n = 1 ∨ n.Prime

Sources

Ivan V. Morozov, "On Quotients of a More General Theorem of Wilson", Theorem 2.

Uses 1

Statement usesMorozov's sign-adjusted Wilson quotient sum

TheoremThe Wilson quotient sum Z(n) modulo n#●ready to prove

Let \(n \ge 1\) be a natural number. Morozov's Wilson quotient sum \(Z(n)\) is an integer; moreover \(Z(n) \equiv 1 \pmod{n}\) if \(n\) is neither \(1\) nor prime, and \(Z(n) \equiv -1 \pmod{n}\) if \(n = 1\) or \(n\) is prime.

theorem_wanted exists_int_eq_wilsonQuotientZ_and_modEq
    (n : ℕ) (hn : 1 ≤ n) :
    ∃ z : ℤ, (z : ℚ) = wilsonQuotientZ n ∧
      ((¬(n = 1 ∨ n.Prime) → z ≡ 1 [ZMOD (n : ℤ)]) ∧
        ((n = 1 ∨ n.Prime) → z ≡ -1 [ZMOD (n : ℤ)]))

Sources

Ivan V. Morozov, "On Quotients of a More General Theorem of Wilson", Theorem 3.

Uses 1

Statement usesMorozov's Wilson quotient sum

TheoremA primality criterion from the Wilson quotient sum Z(2n − 1)#●ready to prove

For every natural number \(n \ge 1\), Morozov's Wilson quotient sum \(Z(2n - 1)\) is an integer, and it is divisible by \(n\) if and only if \(n = 1\) or \(n\) is prime.

theorem_wanted exists_int_eq_wilsonQuotientZ_two_mul_sub_one_modEq_zero_iff
    (n : ℕ) (hn : 1 ≤ n) :
    ∃ z : ℤ, (z : ℚ) = wilsonQuotientZ (2 * n - 1) ∧
      ((z ≡ 0 [ZMOD (n : ℤ)]) ↔ n = 1 ∨ n.Prime)

Sources

Ivan V. Morozov, "On Quotients of a More General Theorem of Wilson", Theorem 4.

Uses 1

Statement usesMorozov's Wilson quotient sum

TheoremThe sign-adjusted Wilson quotient sum Z⁺(2n) modulo 2n#●ready to prove

Let \(n \ge 1\) be a natural number. Morozov's sign-adjusted Wilson quotient sum \(Z^+(2n)\) is an integer; it satisfies \(Z^+(2n) \equiv 0 \pmod{2n}\) if \(n = 2\) or \(n\) is neither \(1\) nor prime, and \(Z^+(2n) \equiv n + 1 \pmod{2n}\) if \(n\) is an odd prime.

theorem_wanted exists_int_eq_wilsonQuotientZPlus_two_mul_and_modEq
    (n : ℕ) (hn : 1 ≤ n) :
    ∃ z : ℤ, (z : ℚ) = wilsonQuotientZPlus (2 * n) ∧
      (((n = 2 ∨ ¬(n = 1 ∨ n.Prime)) → z ≡ 0 [ZMOD (2 * n : ℤ)]) ∧
        (((n.Prime ∧ n ≠ 2) → z ≡ (n : ℤ) + 1 [ZMOD (2 * n : ℤ)])))

Sources

Ivan V. Morozov, "On Quotients of a More General Theorem of Wilson", Theorem 5, equations (8) and (9).

Uses 1

Statement usesMorozov's sign-adjusted Wilson quotient sum

TheoremA Bernoulli–harmonic congruence for the sign-adjusted Wilson quotient sum#●ready to prove

Let \(p\) be an odd prime, let \(B_m\) denote the Bernoulli numbers, and let \(H_k = \sum_{j=1}^{k} 1/j\) denote the harmonic numbers, with \(H_0 = 0\). Then \(p\) divides the numerator, in lowest terms, of the rational number

\[Z^+(p) - \Bigl(B_{2(p-1)} - B_{p-1} - \sum_{k=0}^{p-1} (-1)^k H_k\Bigr),\]

where \(Z^+(p)\) is Morozov's sign-adjusted Wilson quotient sum.

This is the congruence obtained by summing the paper's Equation (7). The printed simplification of the alternating harmonic sum to \(H_{p-1}/2\) is false already at \(p = 3\).

theorem_wanted prime_dvd_num_wilsonQuotientZPlus_sub_bernoulli_alternating
    (p : ℕ) (hp : p.Prime) (hpodd : p % 2 = 1) :
    (p : ℤ) ∣ (wilsonQuotientZPlus p -
      (bernoulli (2 * (p - 1)) - bernoulli (p - 1) -
        ∑ k ∈ Finset.range p, (-1 : ℚ) ^ k * harmonic k)).num

Sources

Ivan V. Morozov, "On Quotients of a More General Theorem of Wilson", Theorem 6 and Equation (7).

Uses 1

Statement usesMorozov's sign-adjusted Wilson quotient sum

7 fully proved8 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.