Theorems · Definition · number theory

DirichletCharacter.rootNumber

{N : ℕ} → [NeZero N] → DirichletCharacter ℂ N → ℂ

Global root number of χ (for χ primitive; junk otherwise). Defined as gaussSum χ stdAddChar / I ^ a / N ^ (1 / 2), where a = 0 if even, a = 1 if odd. (The factor 1 / I ^ a is the Archimedean root number.) This is a complex number of absolute value 1.

Defined in

Mathlib.NumberTheory.LSeries.DirichletContinuation

Cited by

3 results in Mathlib

Foundations

Depth 205 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NeZero