Commit 2023-09-19 14:15 96747a0e

View on Github →

feat: Dirichlet character (#7010)

depends on: #7013

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/DirichletCharacter/Basic.lean

added theorem DirichletCharacter.eval_modulus_sub

added theorem DirichletCharacter.periodic

added theorem DirichletCharacter.toUnitHom_eq_char'

added theorem DirichletCharacter.toUnitHom_eq_iff

Modified Mathlib/NumberTheory/LegendreSymbol/MulCharacter.lean

added theorem MulChar.coe_toMonoidHom