Multiplicativity of $\tau$ (Mordell 1917)

Open

RamanujanPetersson.tau_multiplicative

by Lucas · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

modular-formsnumber-theory

Ramanujan's tau function is multiplicative: $\tau(1)=1$ , and for all natural numbers $m,n$ with $\gcd(m,n)=1$ ,

\tau(mn)=\tau(m)\,\tau(n).

This is the first of Ramanujan's 1916 conjectures, proved by Mordell in 1917. It is what makes the Euler product of $L(s,\tau)$ possible.

Formalization Note $\tau$ is RamanujanPetersson.tau, the $n$ -th coefficient of Mathlib's $q$ -expansion (period $1$ ) of ModularForm.discriminant, valued in $\mathbb C$ .

Preamble

import Mathlib
import Definitions.Def_RamanujanPetersson_tau

open UpperHalfPlane Filter Asymptotics MatrixGroups
open scoped Real

Formal statement

namespace RamanujanPetersson

theorem tau_multiplicative :
    tau 1 = 1 ∧ ∀ m n : ℕ, m.Coprime n → tau (m * n) = tau m * tau n := by sorry

end RamanujanPetersson

Source

Wikipedia, "Ramanujan–Petersson conjecture", https://en.wikipedia.org/w/index.php?title=Ramanujan%E2%80%93Petersson_conjecture&oldid=1369029052 (PDF snapshot supplied by the proposer, 9 pp.), section "Ramanujan conjecture", Ramanujan's conjecture 1 ("

\tau

is multiplicative"); proved by Mordell (1917) per the following paragraph

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Multiplicativity of τ\tauτ (Mordell 1917)

Multiplicativity of $\tau$ (Mordell 1917)