Carmichael numbers

This file defines Carmichael numbers and proves Korselt's criterion about them.

Main definitions

• Nat.IsCarmichael: a predicate for Carmicheal numbers

Main results

• Nat.IsCarmichael_iff_korselt: Korselt's criterion for Carmichael numbers
• Nat.isCarmichael_561: 561 is a Carmichael number

TODO

• Prove (in a computationally efficient manner) that there are no Carmichael numbers less than 561.

References

https://en.wikipedia.org/wiki/Carmichael_number

def Nat.IsCarmichael (n : ℕ) : Prop

We say a natural number n is a Carmichael number if it is greater than 2, composite and for all natural numbers b coprime to n we have n ∣ b ^ (n - 1) - 1.

Equations

• n.IsCarmichael = (2 < n ∧ ¬Nat.Prime n ∧ ∀ (b : ℕ), b.Coprime n → n.ProbablePrime b)

theorem Nat.IsCarmichael.two_lt {n : ℕ} (h : n.IsCarmichael) : 2 < n

theorem Nat.IsCarmichael.neZero {n : ℕ} (h : n.IsCarmichael) : NeZero n

theorem Nat.IsCarmichael.not_prime {n : ℕ} (h : n.IsCarmichael) : ¬Prime n

theorem Nat.IsCarmichael.probablePrime_of_coprime {n b : ℕ} (h : n.IsCarmichael) (hb : b.Coprime n) : n.ProbablePrime b

theorem Nat.Prime.not_isCarmichael {n : ℕ} (hn : Prime n) : ¬n.IsCarmichael

@[simp]

theorem Nat.not_isCarmichael_zero : ¬IsCarmichael 0

@[simp]

theorem Nat.not_isCarmichael_one : ¬IsCarmichael 1

theorem Nat.IsCarmichael.zmod_unit_pow_sub_one {n : ℕ} (s : (ZMod n)ˣ) (hn : n.IsCarmichael) : s ^ (n - 1) = 1

theorem Nat.IsCarmichael.odd {n : ℕ} (h : n.IsCarmichael) : Odd n

A Carmichael number is odd.

theorem Nat.IsCarmichael.squarefree {n : ℕ} (h : n.IsCarmichael) : Squarefree n

A Carmichael number is squarefree.

theorem Nat.IsCarmichael.carmichael_dvd_sub_one {n : ℕ} (h : n.IsCarmichael) : ArithmeticFunction.carmichael n ∣ n - 1

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

theorem Nat.isCarmichael_iff_korselt {n : ℕ} : n.IsCarmichael ↔ 2 < n ∧ ¬Prime n ∧ Squarefree n ∧ ∀ (p : ℕ), Prime p → p ∣ n → p - 1 ∣ n - 1

Korselt's criterion for Carmichael numbers: n is a Carmichael number if and only if it is greater than two, composite, squarefree, and for each prime divisor p of n, we have p - 1 ∣ n - 1.

theorem Nat.isCarmichael_iff_korselt_primeFactorsList {n : ℕ} : n.IsCarmichael ↔ 2 < n ∧ ¬Prime n ∧ n.primeFactorsList.Nodup ∧ ∀ p ∈ n.primeFactorsList, p - 1 ∣ n - 1

Korselt's criterion stated in a form suitable for concrete calculations.

theorem Nat.isCarmichael_561 : IsCarmichael 561

561 is a Carmichael number.

theorem Nat.isCarmichael_1105 : IsCarmichael 1105

1105 is a Carmichael number.