Multiplicativity of the Dedekind ψ function #
Theorem statement: ModularCurve.dedekindPsi_mul_of_coprime
(279a2b31-54aa-5736-b408-0c9a53ca3d30), by Claude, 2026-09-05.
Proof: submission cdb27e77-3b26-5ce0-beb7-e90f5223354a, by Claude, 2026-09-05 (ACCEPTED); locally
adapted.
For natural numbers $M$ and $N$ that are coprime, the function $\psi$ defined by $$\psi(N) = \sum_{\substack{d \mid N \\ d \text{ squarefree}}} N/d,$$ the sum being over the divisors $d$ of $N$
in the sense of Nat.divisors (so over an empty set when $N = 0$) that are squarefree, with $N/d$
the quotient of natural numbers, which is exact since $d$ divides $N$, satisfies $\psi(MN) = \psi(M)\,\psi(N)$. No positivity hypothesis is imposed on $M$ or $N$: the case where one of them
vanishes is covered, both sides then being $0$ unless the other is $1$. Thus dedekindPsi is
multiplicative on coprime pairs; for $N \geq 1$ its value is $N \prod_{p \mid N} (1 + 1/p)$, but
that closed form is not what the statement asserts.
This is the multiplicativity, on coprime arguments, of the Dedekind $\psi$ function, which computes the index of $\Gamma_0(N)$ in $\mathrm{SL}_2(\mathbb{Z})$. It is used throughout the index and genus computations for the modular curves $X_0(N)$ and their relatives, for instance in reducing such quantities to prime powers.
Explanation of the source proof #
Proof transplanted from the FLT repository: https://github.com/anthropics/fermats-last-theorem/blob/aa2d8b34692b16c70f699536de0d8e75b9a3e9ef/P2M/Sol/S_ModularCurve_dedekindPsi_mul_of_coprime.lean
<!-- Generated by add_prove2me_provenance.py -->