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

source

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)

Instances For

source

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

2 < n

source

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

NeZero n

source

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

¬Prime n

source

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

n.ProbablePrime b

source

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

¬n.IsCarmichael

source

@[simp]

theorem Nat.not_isCarmichael_zero :

¬IsCarmichael 0

source

@[simp]

theorem Nat.not_isCarmichael_one :

¬IsCarmichael 1

source

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

s ^ (n - 1) = 1

source

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

Odd n

A Carmichael number is odd.

source

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

Squarefree n

A Carmichael number is squarefree.

source

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

ArithmeticFunction.carmichael n ∣ n - 1

source

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

p - 1 ∣ n - 1

source

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.

source