Carmichael and Giuga Numbers

Definitions of the two key number classes used in the reduction of the Agoh–Giuga conjecture.

def IsCarmichaelNumber (n : ℕ) : Prop

A Carmichael number is a composite n > 1 such that a^(n-1) ≡ 1 (mod n) for every a coprime to n.

Equations

• IsCarmichaelNumber n = (¬Nat.Prime n ∧ 1 < n ∧ ∀ (a : ZMod n), a.val.Coprime n → a ^ (n - 1) = 1)

def IsGiugaNumber (n : ℕ) : Prop

A Giuga number is a composite n > 1 such that p ∣ (n/p - 1) for every prime factor p of n.

Equations

• IsGiugaNumber n = (¬Nat.Prime n ∧ 1 < n ∧ ∀ p ∈ n.primeFactors, p ∣ n / p - 1)