Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Analytic Extension of Nontrivial Cyclotomic Artin Series

Abstract

Analytic Extension of Nontrivial Cyclotomic Artin Series.

Theorem 1.1 (Analytic Extension of Nontrivial Cyclotomic Artin Series).

Lean statement: D5/S3/Analytic/Zeta/NumberField/ZetaProductAnalytic.artinLSeries_analytic_extension

Proof. Machine-checked in Lean as D5/S3/Analytic/Zeta/NumberField/ZetaProductAnalytic.artinLSeries_analytic_extension (✓ 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 nontrivial character of a cyclotomic Galois extension L/K with m modulo four unequal to two, there is a function analytic on the half-plane Re(s) > 1 - 1/[K:Q]. On Re(s) > 1 it agrees with the Dirichlet series weighted by the character on nonzero ideals of K.

References