# Documentation

Mathlib.NumberTheory.DirichletCharacter.Basic

# Dirichlet Characters #

Let R be a commutative monoid with zero. A Dirichlet character χ of level n over R is a multiplicative character from ZMod n to R sending non-units to 0. We then obtain some properties of toUnitHom χ, the restriction of χ to a group homomorphism (ZMod n)ˣ →* Rˣ.

Main definitions:

• DirichletCharacter: The type representing a Dirichlet character.
• changeLevel: Extend the Dirichlet character χ of level n to level m, where n divides m.

## TODO #

• properties of the conductor

## Tags #

dirichlet character, multiplicative character

@[inline, reducible]
abbrev DirichletCharacter (R : Type) (n : ) :

The type of Dirichlet characters of level n.

Instances For
theorem DirichletCharacter.toUnitHom_eq_char' {R : Type} {n : } (χ : ) {a : ZMod n} (ha : ) :
χ a = ↑(↑() ())
theorem DirichletCharacter.toUnitHom_eq_iff {R : Type} {n : } (χ : ) (ψ : ) :
χ = ψ
theorem DirichletCharacter.eval_modulus_sub {R : Type} {n : } (χ : ) (x : ZMod n) :
χ (n - x) = χ (-x)
theorem DirichletCharacter.periodic {R : Type} {n : } (χ : ) {m : } (hm : n m) :
noncomputable def DirichletCharacter.changeLevel {R : Type} {n : } {m : } (hm : n m) :

A function that modifies the level of a Dirichlet character to some multiple of its original level.

Instances For
theorem DirichletCharacter.changeLevel_def {R : Type} {n : } (χ : ) {m : } (hm : n m) :
theorem DirichletCharacter.changeLevel_def' {R : Type} {n : } (χ : ) {m : } (hm : n m) :
@[simp]
theorem DirichletCharacter.changeLevel_self {R : Type} {n : } (χ : ) :
↑(DirichletCharacter.changeLevel (_ : n n)) χ = χ
theorem DirichletCharacter.changeLevel_trans {R : Type} {n : } (χ : ) {m : } {d : } (hm : n m) (hd : m d) :
↑(DirichletCharacter.changeLevel (_ : n d)) χ = ↑() ()
theorem DirichletCharacter.changeLevel_eq_cast_of_dvd {R : Type} {n : } (χ : ) {m : } (hm : n m) (a : (ZMod m)ˣ) :
↑() a = χ a
def DirichletCharacter.FactorsThrough {R : Type} {n : } (χ : ) (d : ) :

χ of level n factors through a Dirichlet character χ₀ of level d if d ∣ n and χ₀ = χ ∘ (ZMod n → ZMod d).

Instances For
theorem DirichletCharacter.FactorsThrough.dvd {R : Type} {n : } (χ : ) {d : } (h : ) :
d n

The fact that d divides n when χ factors through a Dirichlet character at level d

noncomputable def DirichletCharacter.FactorsThrough.χ₀ {R : Type} {n : } (χ : ) {d : } (h : ) :

The Dirichlet character at level d through which χ factors

Instances For
theorem DirichletCharacter.FactorsThrough.eq_changeLevel {R : Type} {n : } (χ : ) {d : } (h : ) :
χ = ↑(DirichletCharacter.changeLevel (_ : d n)) ()

The fact that χ factors through χ₀ of level d

def DirichletCharacter.conductorSet {R : Type} {n : } (χ : ) :

The set of natural numbers for which a Dirichlet character is periodic.

Instances For
theorem DirichletCharacter.mem_conductorSet_iff {R : Type} {n : } (χ : ) {x : } :
theorem DirichletCharacter.mem_conductorSet_dvd {R : Type} {n : } (χ : ) {x : } (hx : ) :
x n
noncomputable def DirichletCharacter.conductor {R : Type} {n : } (χ : ) :

The minimum natural number n for which a Dirichlet character is periodic. The Dirichlet character χ can then alternatively be reformulated on ℤ/nℤ.

Instances For