The coefficients $a_n$ of the Hasse–Weil L-series of $E/\mathbb{Q}$ are multiplicative

Proved

BSD.lFunction_isMultiplicative

by korbonits · Sep 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

birch-swinnerton-dyerelliptic-curvesl-functionsnumber-theory

Let $E$ be a Weierstrass curve over $\mathbb{Q}$ and let $L(E,s) = \sum_{n \ge 1} a_n n^{-s}$ be its Hasse–Weil L-series, defined as the formal Euler product over all primes $p$ of the local factors $1/f_p(p^{-s})$ , where $f_p(T)$ is $1 - a_p T + p T^2$ , $1 - T$ , $1 + T$ or $1$ according as a model of $E$ minimal at $p$ has good, split multiplicative, non-split multiplicative or additive reduction. Then the coefficient function $n \mapsto a_n$ is multiplicative:

a_1 = 1, \qquad a_{mn} = a_m\, a_n \quad \text{whenever } \gcd(m,n) = 1.

This is the arithmetic content of the Euler product expansion (Silverman, Appendix C, §16): $a_n = \prod_{p^k \,\|\, n} a_{p^k}$ , where $a_{p^k}$ is the $k$ -th coefficient of the power series $1/f_p(T)$ . It reduces every bound or congruence for the $a_n$ to the prime-power case.

Formalization Note $a_n$ is Mathlib's WeierstrassCurve.LFunction W n, an ArithmeticFunction ℤ defined as ArithmeticFunction.eulerProduct of the local factors localEulerFactor indexed by the height-one primes of $\mathcal{O}_{\mathbb{Q}}$ ; each local factor substitutes $T = q^{-s}$ with $q$ the cardinality of the residue field of the $\mathfrak{p}$ -adic completion. No hypothesis on the discriminant is needed.

Preamble

import Definitions.Def_BSD
import Mathlib

Formal statement

namespace BSD
theorem lFunction_isMultiplicative (W : WeierstrassCurve ℚ) :
    W.LFunction.IsMultiplicative := by sorry
end BSD

Source

J. H. Silverman, The Arithmetic of Elliptic Curves, 2nd ed., GTM 106, Springer 2009, Appendix C, §16 (the L-series of E/Q as an Euler product, expanded as a Dirichlet series); A. Wiles, The Birch and Swinnerton-Dyer Conjecture (Clay Millennium Problem description, 2000), p. 2 (definition of L(C,s) as an Euler product). Formalized against Mathlib's WeierstrassCurve.LFunction (Mathlib.AlgebraicGeometry.EllipticCurve.LFunction).

View graph

The coefficients ana_nan​ of the Hasse–Weil L-series of E/QE/\mathbb{Q}E/Q are multiplicative

The coefficients $a_n$ of the Hasse–Weil L-series of $E/\mathbb{Q}$ are multiplicative