feat: Dirichlet character (#7010)

- [x] depends on: #7013 



Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: laughinggas <58670661+laughinggas@users.noreply.github.com>

Author: mo271

Mathlib.lean

@@ -2560,6 +2560,7 @@ import Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
 import Mathlib.NumberTheory.Cyclotomic.Rat
 import Mathlib.NumberTheory.Dioph
 import Mathlib.NumberTheory.DiophantineApproximation
+import Mathlib.NumberTheory.DirichletCharacter.Basic
 import Mathlib.NumberTheory.Divisors
 import Mathlib.NumberTheory.FLT.Basic
 import Mathlib.NumberTheory.FLT.Four

Mathlib/NumberTheory/DirichletCharacter/Basic.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2023 Ashvni Narayanan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ashvni Narayanan, Moritz Firsching
+-/
+import Mathlib.Algebra.Periodic
+import Mathlib.NumberTheory.LegendreSymbol.MulCharacter
+import Mathlib.Data.ZMod.Algebra
+
+/-!
+# 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.
+
+## TODO
+
+- `change_level`: Extend the Dirichlet character χ of level `n` to level `m`, where `n` divides `m`.
+- definition of conductor
+
+## Tags
+
+dirichlet character, multiplicative character
+-/
+
+/-- The type of Dirichlet characters of level `n`. -/
+abbrev DirichletCharacter (R : Type) [CommMonoidWithZero R] (n : ℕ) := MulChar (ZMod n) R
+
+open MulChar
+variable {R : Type} [CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n)
+
+namespace DirichletCharacter
+lemma toUnitHom_eq_char' {a : ZMod n} (ha : IsUnit a) :
+  χ a = χ.toUnitHom ha.unit := by simp
+
+lemma toUnitHom_eq_iff (ψ : DirichletCharacter R n) :
+  toUnitHom χ = toUnitHom ψ ↔ χ = ψ := by simp
+
+lemma eval_modulus_sub (x : ZMod n) :
+  χ (n - x) = χ (-x) := by simp
+
+lemma periodic {m : ℕ} (hm : n ∣ m) : Function.Periodic χ m := by
+  intro a
+  rw [← ZMod.nat_cast_zmod_eq_zero_iff_dvd] at hm
+  simp only [hm, add_zero]
+
+end DirichletCharacter

Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean

@@ -237,6 +237,10 @@ theorem equivToUnitHom_symm_coe (f : Rˣ →* R'ˣ) (a : Rˣ) : equivToUnitHom.s
   ofUnitHom_coe f a
 #align mul_char.equiv_unit_hom_symm_coe MulChar.equivToUnitHom_symm_coe
 
+@[simp]
+lemma coe_toMonoidHom [CommMonoid R] (χ : MulChar R R')
+    (x : R) : χ.toMonoidHom x = χ x := rfl
+
 /-!
 ### Commutative group structure on multiplicative characters