The Carmichael function

Main definitions

• ArithmeticFunction.Carmichael: the Carmichael function λ, also known as the reduced totient function.

Main results

• A formula for λ n in terms of the prime factorization of n, given by the following theorems: carmichael_two_pow_of_le_two, carmichael_two_pow_of_ne_two, carmichael_pow_of_prime_ne_two, and carmichael_factorization.

Notation

We use the standard notation λ to represent the Carmichael function, which is accessible in the scope ArithmeticFunction.Carmichael. Since the notation conflicts with the anonymous function notation, it is impossible to use this notation in statements, but the pretty-printer will use it when showing the goal state.

Tags

arithmetic functions, totient

def ArithmeticFunction.Carmichael : ArithmeticFunction ℕ

λ is the Carmichael function, also known as the reduced totient function, defined as the exponent of the unit group of ZMod n.

Equations

• ArithmeticFunction.Carmichael = { toFun := fun (x : ℕ) => match x with | 0 => 0 | n.succ => Nat.find ⋯, map_zero' := ArithmeticFunction.Carmichael._proof_3 }

def ArithmeticFunction.Carmichael.«termλ» : Lean.ParserDescr

λ is the Carmichael function, also known as the reduced totient function, defined as the exponent of the unit group of ZMod n.

Equations

• ArithmeticFunction.Carmichael.«termλ» = Lean.ParserDescr.node `ArithmeticFunction.Carmichael.«termλ» 1024 (Lean.ParserDescr.symbol "λ")

theorem ArithmeticFunction.carmichael_eq_exponent {n : ℕ} (hn : n ≠ 0) : Carmichael n = Monoid.exponent (ZMod n)ˣ

theorem ArithmeticFunction.carmichael_eq_exponent' (n : ℕ) [NeZero n] : Carmichael n = Monoid.exponent (ZMod n)ˣ

This takes in an NeZero n instance instead of an n ≠ 0 hypothesis.

@[simp]

theorem ArithmeticFunction.pow_carmichael {n : ℕ} (a : (ZMod n)ˣ) : a ^ Carmichael n = 1

theorem ArithmeticFunction.carmichael_dvd_totient (n : ℕ) : Carmichael n ∣ n.totient

theorem ArithmeticFunction.carmichael_dvd {a b : ℕ} (h : a ∣ b) : Carmichael a ∣ Carmichael b

theorem ArithmeticFunction.carmichael_lcm (a b : ℕ) : Carmichael (a.lcm b) = (Carmichael a).lcm (Carmichael b)

theorem ArithmeticFunction.carmichael_mul {a b : ℕ} (h : a.Coprime b) : Carmichael (a * b) = (Carmichael a).lcm (Carmichael b)

theorem ArithmeticFunction.carmichael_finset_lcm {α : Type u_2} (s : Finset α) (f : α → ℕ) : Carmichael (s.lcm f) = s.lcm (⇑Carmichael ∘ f)

theorem ArithmeticFunction.carmichael_finset_prod {α : Type u_2} {s : Finset α} {f : α → ℕ} (h : (↑s).Pairwise (Function.onFun Nat.Coprime f)) : Carmichael (s.prod f) = s.lcm (⇑Carmichael ∘ f)

theorem ArithmeticFunction.carmichael_factorization (n : ℕ) [NeZero n] : Carmichael n = n.primeFactors.lcm fun (p : ℕ) => Carmichael (p ^ n.factorization p)

theorem ArithmeticFunction.carmichael_two_pow_of_le_two_eq_totient {n : ℕ} (hn : n ≤ 2) : Carmichael (2 ^ n) = (2 ^ n).totient

@[simp]

theorem ArithmeticFunction.carmichael_two_pow_of_le_two {n : ℕ} (hn : n ≤ 2) : Carmichael (2 ^ n) = 2 ^ (n - 1)

Note that 2 ^ (n - 1) = 1 when n = 0.

@[simp]

theorem ArithmeticFunction.carmichael_two_pow_of_ne_two {n : ℕ} (hn : n ≠ 2) : Carmichael (2 ^ n) = 2 ^ (n - 2)

Note that 2 ^ (n - 2) = 1 when n ≤ 1.

theorem ArithmeticFunction.two_mul_carmichael_two_pow_of_three_le_eq_totient {n : ℕ} (hn : 3 ≤ n) : 2 * Carmichael (2 ^ n) = (2 ^ n).totient

@[simp]

theorem ArithmeticFunction.carmichael_pow_of_prime_ne_two {p : ℕ} (n : ℕ) (hp : Nat.Prime p) (hp₂ : p ≠ 2) : Carmichael (p ^ n) = (p ^ n).totient