Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Zeta Product

Abstract

Zeta Product.

Theorem 1.1 (Zeta Product).

Lean statement: D5/S3/Analytic/Zeta/NumberField/ZetaProduct.artinLSeries_one_ne_zero

Proof. Machine-checked in Lean as D5/S3/Analytic/Zeta/NumberField/ZetaProduct.artinLSeries_one_ne_zero (✓ std3). ∎

Citation. Chris Birkbeck and the Chebotarev density contributors (2026). Chebotarev density in Lean. URL: https://github.com/CBirkbeck/chebotarev-density/tree/a00054a0e6bbc394b0e81de750db0cd2efc8bd88.

Commentary.

For a finite abelian cyclotomic Galois extension L/K of modulus m with m ≥ 1 and m % 4 ≠ 2, let χ be a nontrivial Galois character. Every function F analytic on Re(s) > 1 - 1/[K:ℚ] that agrees on Re(s) > 1 with the χ-weighted nonzero-ideal Dirichlet series satisfies F(1) ≠ 0.

References