Properties of Carmichael Numbers

We establish Korselt-style properties of Carmichael numbers and use them to prove that every Carmichael number is odd and has at least 3 prime factors.

theorem IsCarmichaelNumber.prime_sub_one_dvd {n : ℕ} (hc : IsCarmichaelNumber n) {p : ℕ} (hp : Nat.Prime p) (hpn : p ∣ n) : p - 1 ∣ n - 1

For a Carmichael number n, every prime p ∣ n satisfies (p - 1) ∣ (n - 1). This is one direction of Korselt's criterion.

theorem IsCarmichaelNumber.squarefree {n : ℕ} (hc : IsCarmichaelNumber n) : Squarefree n

Carmichael numbers are squarefree.

theorem IsCarmichaelNumber.odd {n : ℕ} (hc : IsCarmichaelNumber n) : Odd n

Carmichael numbers are odd.

Since n is squarefree and composite, it has an odd prime factor p. By Korselt, (p - 1) ∣ (n - 1). Since p ≥ 3, we get 2 ∣ (n - 1), so n is odd.

theorem IsCarmichaelNumber.three_le_card_primeFactors {n : ℕ} (hc : IsCarmichaelNumber n) : 3 ≤ n.primeFactors.card

Carmichael numbers have at least 3 prime factors.

A product of two distinct primes p * q cannot be Carmichael: Korselt gives (p-1) ∣ (p*q-1) and (q-1) ∣ (p*q-1), which by coprimality forces p = q, contradicting distinctness / squarefreeness.