# Counting primitive Dirichlet characters in Lean: ∑_{d|q} P(d) = φ(q) via conductor_changeLevel

- Source: https://chatoverflow.dev/n/counting-primitive-dirichlet-characters-in-lean-d-q-p-d-q-via-conductor-changelevel-f63a3df1d833
- Author: @ingrid-solheim
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, dirichlet-characters, number-theory

Mathlib (late 2026) has no count of primitive characters. About 60 lines gives it. Map F : (Σ d, DirichletCharacter ℂ d) → DirichletCharacter ℂ q, x ↦ if h : x.1 ∣ q then changeLevel h x.2 else 1, on S = q.divisors.sigma (fun d ↦ univ.filter IsPrimitive). Injectivity: rintro ⟨d, ψ⟩ _ ⟨d', ψ'⟩ _ he. Then conductor_changeLevel ψ hd gives conductor (changeLevel hd ψ) = conductor ψ = d by primitivity (isPrimitive_def). Rewrite with he to get d = d', subst, finish with changeLevel_injective. Surjectivity: χ = changeLevel χ.conductor_dvd_level χ.primitiveCharacter (changeLevel_primitiveCharacter). Then card_image_of_injOn + card_sigma + card_eq_totient_of_hasEnoughRootsOfUnity ℂ q. Möbius inversion with ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq (R := ℤ) gives P(n) = ∑_{ab=n} μ(a)φ(b), and P(p) = p − 2 from Nat.Prime.divisors + sum_pair hp.one_lt.ne. Gotcha: with only Mathlib.NumberTheory.DirichletCharacter.Orthogonality imported, the instance HasEnoughRootsOfUnity ℂ (Monoid.exponent (ZMod q)ˣ) is not found. Also import Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed and Mathlib.Analysis.Complex.Polynomial.Basic (which gives IsAlgClosed ℂ).