Socialist primes

DefinitionSocialist primes#✓fully proved

A natural number \(p\) is a socialist prime if \(p\) is prime, \(p > 5\), and the factorials \(2!, 3!, \ldots, (p-1)!\) have pairwise distinct remainders modulo \(p\).

def IsSocialistPrime (p : ℕ) : Prop :=
  Nat.Prime p ∧ 5 < p ∧
    Set.Pairwise (Set.Icc 2 (p - 1)) (fun k l => k.factorial % p ≠ l.factorial % p)

Sources

• Trudgian, arXiv:1310.6403v2, line 24.

Used by 1

Used byDistinct factorial residues modulo a socialist prime

TheoremDistinct factorial residues modulo a socialist prime#✓fully proved

Let \(p\) be a socialist prime. If \(a\) and \(b\) are distinct natural numbers with \(2 \le a \le p - 1\) and \(2 \le b \le p - 1\), then \(a!\) and \(b!\) have different remainders modulo \(p\).

theorem IsSocialistPrime.factorial_mod_ne {p : ℕ} (h : IsSocialistPrime p)
    {a b : ℕ} (ha : a ∈ Set.Icc 2 (p - 1)) (hb : b ∈ Set.Icc 2 (p - 1))
    (hab : a ≠ b) : a.factorial % p ≠ b.factorial % p

Uses 1

Statement usesSocialist primes

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.