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:

TODO #

Tags #

dirichlet character, multiplicative character

@[inline, reducible]

The type of Dirichlet characters of level n.

Instances For
    theorem DirichletCharacter.toUnitHom_eq_char' {R : Type} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) {a : ZMod n} (ha : IsUnit a) :
    χ a = ↑(↑(MulChar.toUnitHom χ) (IsUnit.unit ha))
    theorem DirichletCharacter.eval_modulus_sub {R : Type} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) (x : ZMod n) :
    χ (n - x) = χ (-x)
    theorem DirichletCharacter.periodic {R : Type} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) {m : } (hm : n m) :
    noncomputable def DirichletCharacter.changeLevel {R : Type} [CommMonoidWithZero R] {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_eq_cast_of_dvd {R : Type} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R n) {m : } (hm : n m) (a : (ZMod m)ˣ) :
      ↑(↑(DirichletCharacter.changeLevel hm) χ) a = χ a

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

      Instances For

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

        The Dirichlet character at level d through which χ factors

        Instances For

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

          Instances For
            noncomputable def DirichletCharacter.conductor {R : Type} [CommMonoidWithZero R] {n : } (χ : DirichletCharacter R 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