2.3. Even and odd characters
Definition2.3.1
A Dirichlet character \chi is even if \chi(-1)=1 and odd if
\chi(-1)=-1.
Lean code for Definition2.3.1●1 definition
Associated Lean declarations
-
DirichletCharacter.Even[complete]
Associated Lean declarations
-
DirichletCharacter.Even[complete]
-
defdefined in Mathlib/NumberTheory/DirichletCharacter/Basic.leancomplete
def DirichletCharacter.Even.{u_2} {S : Type u_2} [CommRing S] {m : ℕ} (ψ : DirichletCharacter S m) : Prop
def DirichletCharacter.Even.{u_2} {S : Type u_2} [CommRing S] {m : ℕ} (ψ : DirichletCharacter S m) : Prop
A Dirichlet character is even if its value at -1 is 1.
Exactly half of the characters modulo p are even and exactly half are odd. The
even characters are precisely those that factor through the quotient
(\mathbb{Z}/p\mathbb{Z})^\times / \{\pm 1\}, which is the Galois group of the
maximal real subfield \mathbb{Q}(\zeta_p)^+. This parity distinction is the source
of the even/odd decomposition in the analytic class number formula.
Finally, because p is prime, every non-trivial Dirichlet character modulo p is
primitive. Hence the functional equation for primitive Dirichlet L-functions
applies to every odd character that appears later.